1
Я пытаюсь доказать что-то вроде этого:Применения функциональной экстенсиональности к функциям с 2 аргументами в Coq
(fun (i : nat) (ic : i < S n) => ...) = (fun (i : nat) (ip : i < S n) => ...)
Это звучит как задача для apply functional_extensionality, но она не унифицировать. Я подозреваю, что мне нужно как-то применить его дважды, но не знаю, как это сделать.
Проблема заключается не в том, что вам нужно, чтобы применить его в два раза, то, что второй аргумент типа зависит от первого. Поэтому вы должны применить зависимую версию 'functional_extensionality_dep' (которая выполняется тактикой' extality'). Более того, если тела функций идентичны, вы можете использовать прямо «рефлексивность». – eponier