lemma extensional_perm : ∀T.∀f,g.(∀x.f x = g x) → perm T f = perm T g.
intro;elim T
[4:whd in ⊢ (??%%);cut (∀x.flift f 1 x = flift g 1 x)
lemma extensional_perm : ∀T.∀f,g.(∀x.f x = g x) → perm T f = perm T g.
intro;elim T
[4:whd in ⊢ (??%%);cut (∀x.flift f 1 x = flift g 1 x)