(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/pr3/fwd.ma".
+include "Basic-1/pr3/fwd.ma".
-include "LambdaDelta-1/iso/props.ma".
+include "Basic-1/iso/props.ma".
-include "LambdaDelta-1/tlist/props.ma".
+include "Basic-1/tlist/props.ma".
theorem pr3_iso_appls_abbr:
\forall (c: C).(\forall (d: C).(\forall (w: T).(\forall (i: nat).((getl i c
c x1 x5 H9 (Bind x0) (THead (Flat Appl) (lift (S O) O x4) x2) (THead (Flat
Appl) (lift (S O) O x4) x3) (pr3_thin_dx (CHead c (Bind x0) x5) x2 x3 H10
(lift (S O) O x4) Appl)) u2 H7)))))))))))))) H4)) H3)))))))) vs)))))).
+(* COMMENTS
+Initial nodes: 3759
+END *)
theorem pr3_iso_appls_cast:
\forall (c: C).(\forall (v: T).(\forall (t: T).(\forall (vs: TList).(let u1
(pr3_head_12 c x1 x5 H8 (Bind x0) (THead (Flat Appl) (lift (S O) O x4) x2)
(THead (Flat Appl) (lift (S O) O x4) x3) (pr3_thin_dx (CHead c (Bind x0) x5)
x2 x3 H9 (lift (S O) O x4) Appl)) u2 H6)))))))))))))) H3)) H2)))))))) vs)))).
+(* COMMENTS
+Initial nodes: 3297
+END *)
theorem pr3_iso_appl_bind:
\forall (b: B).((not (eq B b Abst)) \to (\forall (v1: T).(\forall (v2:
O) O x4) Appl))) (THead (Flat Appl) (lift (S O) O x4) (lift (S O) O (THead
(Bind x0) x1 x2))) (lift_flat Appl x4 (THead (Bind x0) x1 x2) (S O) O))))
H10))) u2 H6))))))))))))) H3)) H2)))))))))).
+(* COMMENTS
+Initial nodes: 4805
+END *)
theorem pr3_iso_appls_appl_bind:
\forall (b: B).((not (eq B b Abst)) \to (\forall (v: T).(\forall (u:
Appl) (lift (S O) O x4) x2) (THead (Flat Appl) (lift (S O) O x4) x3)
(pr3_thin_dx (CHead c (Bind x0) x5) x2 x3 H10 (lift (S O) O x4) Appl)) u2
H7)))))))))))))) H4)) H3))))))))) vs)))))).
+(* COMMENTS
+Initial nodes: 3571
+END *)
theorem pr3_iso_appls_bind:
\forall (b: B).((not (eq B b Abst)) \to (\forall (vs: TList).(\forall (u:
(Flat Appl) (TApp (lifts (S O) O ts) (lift (S O) O t)) t0) (theads_tapp (Flat
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))).
+(* COMMENTS
+Initial nodes: 1681
+END *)
theorem pr3_iso_beta:
\forall (v: T).(\forall (w: T).(\forall (t: T).(let u1 \def (THead (Flat
Abst))) H3 Abst H17) in (let H23 \def (match (H22 (refl_equal B Abst)) in
False return (\lambda (_: False).(pr3 c (THead (Bind Abbr) v t) u2)) with [])
in H23))))))))) H14)) H13))))))) H9)))))))))))))) H2)) H1)))))))).
+(* COMMENTS
+Initial nodes: 2459
+END *)
theorem pr3_iso_appls_beta:
\forall (us: TList).(\forall (v: T).(\forall (w: T).(\forall (t: T).(let u1
(pr3_head_12 c x1 x5 H8 (Bind x0) (THead (Flat Appl) (lift (S O) O x4) x2)
(THead (Flat Appl) (lift (S O) O x4) x3) (pr3_thin_dx (CHead c (Bind x0) x5)
x2 x3 H9 (lift (S O) O x4) Appl)) u2 H6)))))))))))))) H3)) H2)))))))))))) us).
+(* COMMENTS
+Initial nodes: 3345
+END *)