(* This file was automatically generated: do not edit *********************)
-include "ty3/arity.ma".
+include "LambdaDelta-1/ty3/arity.ma".
-include "pc3/nf2.ma".
+include "LambdaDelta-1/pc3/nf2.ma".
-include "nf2/arity.ma".
+include "LambdaDelta-1/nf2/arity.ma".
definition ty3_nf2_inv_abst_premise:
C \to (T \to (T \to Prop))
(\lambda (v: T).(\lambda (_: T).(nf2 (CHead c (Bind Abst) w) v)))) (\lambda
(x4: T).(\lambda (x5: T).(\lambda (H13: (pc3 c (THead (Bind Abst) x0 x4)
(THead (Bind Abst) w u))).(\lambda (_: (ty3 g c x0 x5)).(\lambda (H15: (ty3 g
-(CHead c (Bind Abst) x0) x1 x4)).(and_ind (pc3 c x0 w) (\forall (b:
+(CHead c (Bind Abst) x0) x1 x4)).(land_ind (pc3 c x0 w) (\forall (b:
B).(\forall (u0: T).(pc3 (CHead c (Bind b) u0) x4 u))) (ex4_2 T T (\lambda
(v: T).(\lambda (_: T).(eq T (THead (Bind Abst) x0 x1) (THead (Bind Abst) w
v)))) (\lambda (_: T).(\lambda (w0: T).(ty3 g c w w0))) (\lambda (v: