(* This file was automatically generated: do not edit *********************)
+include "LambdaDelta-1/pr3/fwd.ma".
+include "LambdaDelta-1/iso/props.ma".
-include "pr3/fwd.ma".
-
-include "iso/props.ma".
-
-include "tlist/props.ma".
+include "LambdaDelta-1/tlist/props.ma".
theorem pr3_iso_appls_abbr:
\forall (c: C).(\forall (d: C).(\forall (w: T).(\forall (i: nat).((getl i c
(lifts (S O) O vs) t)) u2))))))))))
\def
\lambda (b: B).(\lambda (H: (not (eq B b Abst))).(\lambda (vs:
-TList).(tlist_ind_rew (\lambda (t: TList).(\forall (u: T).(\forall (t0:
+TList).(tlist_ind_rev (\lambda (t: TList).(\forall (u: T).(\forall (t0:
T).(let u1 \def (THeads (Flat Appl) t (THead (Bind b) u t0)) in (\forall (c:
C).(\forall (u2: T).((pr3 c u1 u2) \to ((((iso u1 u2) \to (\forall (P:
Prop).P))) \to (pr3 c (THead (Bind b) u (THeads (Flat Appl) (lifts (S O) O t)
(lift (S O) O t) t0)) (\lambda (t1: T).(pr3 c (THead (Bind b) u t1) u2)) (let
H3 \def (eq_ind T (THeads (Flat Appl) (TApp ts t) (THead (Bind b) u t0))
(\lambda (t1: T).(pr3 c t1 u2)) H1 (THeads (Flat Appl) ts (THead (Flat Appl)
-t (THead (Bind b) u t0))) (theads_tapp (Flat Appl) ts t (THead (Bind b) u
-t0))) in (let H4 \def (eq_ind T (THeads (Flat Appl) (TApp ts t) (THead (Bind
+t (THead (Bind b) u t0))) (theads_tapp (Flat Appl) t (THead (Bind b) u t0)
+ts)) in (let H4 \def (eq_ind T (THeads (Flat Appl) (TApp ts t) (THead (Bind
b) u t0)) (\lambda (t1: T).((iso t1 u2) \to (\forall (P: Prop).P))) H2
(THeads (Flat Appl) ts (THead (Flat Appl) t (THead (Bind b) u t0)))
-(theads_tapp (Flat Appl) ts t (THead (Bind b) u t0))) in (TList_ind (\lambda
+(theads_tapp (Flat Appl) t (THead (Bind b) u t0) ts)) in (TList_ind (\lambda
(t1: TList).(((\forall (u0: T).(\forall (t2: T).(\forall (c0: C).(\forall
(u3: T).((pr3 c0 (THeads (Flat Appl) t1 (THead (Bind b) u0 t2)) u3) \to
((((iso (THeads (Flat Appl) t1 (THead (Bind b) u0 t2)) u3) \to (\forall (P:
(Bind b) u t0))) (THeads (Flat Appl) ts0 (THead (Bind b) u (THead (Flat Appl)
(lift (S O) O t) t0))) (Flat Appl)) u2 H8) P)))))))))) ts H0 H3 H4))) (THeads
(Flat Appl) (TApp (lifts (S O) O ts) (lift (S O) O t)) t0) (theads_tapp (Flat
-Appl) (lifts (S O) O ts) (lift (S O) O t) t0)) (lifts (S O) O (TApp ts t))
+Appl) (lift (S O) O t) t0 (lifts (S O) O ts))) (lifts (S O) O (TApp ts t))
(lifts_tapp (S O) O t ts))))))))))) vs))).
theorem pr3_iso_beta: