(* This file was automatically generated: do not edit *********************)
-include "sn3/nf2.ma".
+include "LambdaDelta-1/sn3/nf2.ma".
-include "sn3/fwd.ma".
+include "LambdaDelta-1/sn3/fwd.ma".
-include "nf2/iso.ma".
+include "LambdaDelta-1/nf2/iso.ma".
-include "pr3/iso.ma".
-
-include "iso/props.ma".
+include "LambdaDelta-1/pr3/iso.ma".
theorem sn3_pr3_trans:
\forall (c: C).(\forall (t1: T).((sn3 c t1) \to (\forall (t2: T).((pr3 c t1
(pr3_pr2 (CHead c (Bind b) v1) t1 t2 (pr2_change b H c v2 t1 t2 H4
v1)))))))))) t H0))))))).
+theorem sn3_gen_def:
+ \forall (c: C).(\forall (d: C).(\forall (v: T).(\forall (i: nat).((getl i c
+(CHead d (Bind Abbr) v)) \to ((sn3 c (TLRef i)) \to (sn3 d v))))))
+\def
+ \lambda (c: C).(\lambda (d: C).(\lambda (v: T).(\lambda (i: nat).(\lambda
+(H: (getl i c (CHead d (Bind Abbr) v))).(\lambda (H0: (sn3 c (TLRef
+i))).(sn3_gen_lift c v (S i) O (sn3_pr3_trans c (TLRef i) H0 (lift (S i) O v)
+(pr3_pr2 c (TLRef i) (lift (S i) O v) (pr2_delta c d v i H (TLRef i) (TLRef
+i) (pr0_refl (TLRef i)) (lift (S i) O v) (subst0_lref v i)))) d (getl_drop
+Abbr c d v i H))))))).
+
+theorem sn3_cdelta:
+ \forall (v: T).(\forall (t: T).(\forall (i: nat).(((\forall (w: T).(ex T
+(\lambda (u: T).(subst0 i w t u))))) \to (\forall (c: C).(\forall (d:
+C).((getl i c (CHead d (Bind Abbr) v)) \to ((sn3 c t) \to (sn3 d v))))))))
+\def
+ \lambda (v: T).(\lambda (t: T).(\lambda (i: nat).(\lambda (H: ((\forall (w:
+T).(ex T (\lambda (u: T).(subst0 i w t u)))))).(let H_x \def (H v) in (let H0
+\def H_x in (ex_ind T (\lambda (u: T).(subst0 i v t u)) (\forall (c:
+C).(\forall (d: C).((getl i c (CHead d (Bind Abbr) v)) \to ((sn3 c t) \to
+(sn3 d v))))) (\lambda (x: T).(\lambda (H1: (subst0 i v t x)).(subst0_ind
+(\lambda (n: nat).(\lambda (t0: T).(\lambda (t1: T).(\lambda (_: T).(\forall
+(c: C).(\forall (d: C).((getl n c (CHead d (Bind Abbr) t0)) \to ((sn3 c t1)
+\to (sn3 d t0))))))))) (\lambda (v0: T).(\lambda (i0: nat).(\lambda (c:
+C).(\lambda (d: C).(\lambda (H2: (getl i0 c (CHead d (Bind Abbr)
+v0))).(\lambda (H3: (sn3 c (TLRef i0))).(sn3_gen_def c d v0 i0 H2 H3)))))))
+(\lambda (v0: T).(\lambda (u2: T).(\lambda (u1: T).(\lambda (i0:
+nat).(\lambda (_: (subst0 i0 v0 u1 u2)).(\lambda (H3: ((\forall (c:
+C).(\forall (d: C).((getl i0 c (CHead d (Bind Abbr) v0)) \to ((sn3 c u1) \to
+(sn3 d v0))))))).(\lambda (t0: T).(\lambda (k: K).(\lambda (c: C).(\lambda
+(d: C).(\lambda (H4: (getl i0 c (CHead d (Bind Abbr) v0))).(\lambda (H5: (sn3
+c (THead k u1 t0))).(let H_y \def (sn3_gen_head k c u1 t0 H5) in (H3 c d H4
+H_y)))))))))))))) (\lambda (k: K).(\lambda (v0: T).(\lambda (t2: T).(\lambda
+(t1: T).(\lambda (i0: nat).(\lambda (H2: (subst0 (s k i0) v0 t1 t2)).(\lambda
+(H3: ((\forall (c: C).(\forall (d: C).((getl (s k i0) c (CHead d (Bind Abbr)
+v0)) \to ((sn3 c t1) \to (sn3 d v0))))))).(\lambda (u: T).(\lambda (c:
+C).(\lambda (d: C).(\lambda (H4: (getl i0 c (CHead d (Bind Abbr)
+v0))).(\lambda (H5: (sn3 c (THead k u t1))).(K_ind (\lambda (k0: K).((subst0
+(s k0 i0) v0 t1 t2) \to (((\forall (c0: C).(\forall (d0: C).((getl (s k0 i0)
+c0 (CHead d0 (Bind Abbr) v0)) \to ((sn3 c0 t1) \to (sn3 d0 v0)))))) \to ((sn3
+c (THead k0 u t1)) \to (sn3 d v0))))) (\lambda (b: B).(\lambda (_: (subst0 (s
+(Bind b) i0) v0 t1 t2)).(\lambda (H7: ((\forall (c0: C).(\forall (d0:
+C).((getl (s (Bind b) i0) c0 (CHead d0 (Bind Abbr) v0)) \to ((sn3 c0 t1) \to
+(sn3 d0 v0))))))).(\lambda (H8: (sn3 c (THead (Bind b) u t1))).(let H_x0 \def
+(sn3_gen_bind b c u t1 H8) in (let H9 \def H_x0 in (and_ind (sn3 c u) (sn3
+(CHead c (Bind b) u) t1) (sn3 d v0) (\lambda (_: (sn3 c u)).(\lambda (H11:
+(sn3 (CHead c (Bind b) u) t1)).(H7 (CHead c (Bind b) u) d (getl_clear_bind b
+(CHead c (Bind b) u) c u (clear_bind b c u) (CHead d (Bind Abbr) v0) i0 H4)
+H11))) H9))))))) (\lambda (f: F).(\lambda (_: (subst0 (s (Flat f) i0) v0 t1
+t2)).(\lambda (H7: ((\forall (c0: C).(\forall (d0: C).((getl (s (Flat f) i0)
+c0 (CHead d0 (Bind Abbr) v0)) \to ((sn3 c0 t1) \to (sn3 d0 v0))))))).(\lambda
+(H8: (sn3 c (THead (Flat f) u t1))).(let H_x0 \def (sn3_gen_flat f c u t1 H8)
+in (let H9 \def H_x0 in (and_ind (sn3 c u) (sn3 c t1) (sn3 d v0) (\lambda (_:
+(sn3 c u)).(\lambda (H11: (sn3 c t1)).(H7 c d H4 H11))) H9))))))) k H2 H3
+H5))))))))))))) (\lambda (v0: T).(\lambda (u1: T).(\lambda (u2: T).(\lambda
+(i0: nat).(\lambda (_: (subst0 i0 v0 u1 u2)).(\lambda (H3: ((\forall (c:
+C).(\forall (d: C).((getl i0 c (CHead d (Bind Abbr) v0)) \to ((sn3 c u1) \to
+(sn3 d v0))))))).(\lambda (k: K).(\lambda (t1: T).(\lambda (t2: T).(\lambda
+(_: (subst0 (s k i0) v0 t1 t2)).(\lambda (_: ((\forall (c: C).(\forall (d:
+C).((getl (s k i0) c (CHead d (Bind Abbr) v0)) \to ((sn3 c t1) \to (sn3 d
+v0))))))).(\lambda (c: C).(\lambda (d: C).(\lambda (H6: (getl i0 c (CHead d
+(Bind Abbr) v0))).(\lambda (H7: (sn3 c (THead k u1 t1))).(let H_y \def
+(sn3_gen_head k c u1 t1 H7) in (H3 c d H6 H_y))))))))))))))))) i v t x H1)))
+H0)))))).
+
theorem sn3_cpr3_trans:
\forall (c: C).(\forall (u1: T).(\forall (u2: T).((pr3 c u1 u2) \to (\forall
(k: K).(\forall (t: T).((sn3 (CHead c k u1) t) \to (sn3 (CHead c k u2)
x0 H12 (Bind b) x1 (H3 x1 H18 H13)))) H17)))) H15))) t3 H11))))))) H10))
(\lambda (H10: (pr3 (CHead c (Bind b) t1) t2 (lift (S O) O
t3))).(sn3_gen_lift (CHead c (Bind b) t1) t3 (S O) O (sn3_pr3_trans (CHead c
-(Bind b) t1) t2 (sn3_pr2_intro (CHead c (Bind b) t1) t2 (\lambda (t0:
-T).(\lambda (H11: (((eq T t2 t0) \to (\forall (P: Prop).P)))).(\lambda (H12:
-(pr2 (CHead c (Bind b) t1) t2 t0)).(H3 t0 H11 (pr3_pr2 (CHead c (Bind b) t1)
-t2 t0 H12)))))) (lift (S O) O t3) H10) c (drop_drop (Bind b) O c c (drop_refl
-c) t1))) H9)))) H7)))))))))) t H2)))))) u H)))).
+(Bind b) t1) t2 (sn3_sing (CHead c (Bind b) t1) t2 H3) (lift (S O) O t3) H10)
+c (drop_drop (Bind b) O c c (drop_refl c) t1))) H9)))) H7)))))))))) t
+H2)))))) u H)))).
theorem sn3_beta:
\forall (c: C).(\forall (v: T).(\forall (t: T).((sn3 c (THead (Bind Abbr) v
(sn3 c (lift h i t)) (sns3 c (lifts h i t0)) (sn3_lift d t H3 c h i H) (H0
H4)))) H2)))))) ts)))))).
-theorem sn3_gen_def:
- \forall (c: C).(\forall (d: C).(\forall (v: T).(\forall (i: nat).((getl i c
-(CHead d (Bind Abbr) v)) \to ((sn3 c (TLRef i)) \to (sn3 d v))))))
-\def
- \lambda (c: C).(\lambda (d: C).(\lambda (v: T).(\lambda (i: nat).(\lambda
-(H: (getl i c (CHead d (Bind Abbr) v))).(\lambda (H0: (sn3 c (TLRef
-i))).(sn3_gen_lift c v (S i) O (sn3_pr3_trans c (TLRef i) H0 (lift (S i) O v)
-(pr3_pr2 c (TLRef i) (lift (S i) O v) (pr2_delta c d v i H (TLRef i) (TLRef
-i) (pr0_refl (TLRef i)) (lift (S i) O v) (subst0_lref v i)))) d (getl_drop
-Abbr c d v i H))))))).
-
-theorem sn3_cdelta:
- \forall (v: T).(\forall (t: T).(\forall (i: nat).(((\forall (w: T).(ex T
-(\lambda (u: T).(subst0 i w t u))))) \to (\forall (c: C).(\forall (d:
-C).((getl i c (CHead d (Bind Abbr) v)) \to ((sn3 c t) \to (sn3 d v))))))))
-\def
- \lambda (v: T).(\lambda (t: T).(\lambda (i: nat).(\lambda (H: ((\forall (w:
-T).(ex T (\lambda (u: T).(subst0 i w t u)))))).(let H_x \def (H v) in (let H0
-\def H_x in (ex_ind T (\lambda (u: T).(subst0 i v t u)) (\forall (c:
-C).(\forall (d: C).((getl i c (CHead d (Bind Abbr) v)) \to ((sn3 c t) \to
-(sn3 d v))))) (\lambda (x: T).(\lambda (H1: (subst0 i v t x)).(subst0_ind
-(\lambda (n: nat).(\lambda (t0: T).(\lambda (t1: T).(\lambda (_: T).(\forall
-(c: C).(\forall (d: C).((getl n c (CHead d (Bind Abbr) t0)) \to ((sn3 c t1)
-\to (sn3 d t0))))))))) (\lambda (v0: T).(\lambda (i0: nat).(\lambda (c:
-C).(\lambda (d: C).(\lambda (H2: (getl i0 c (CHead d (Bind Abbr)
-v0))).(\lambda (H3: (sn3 c (TLRef i0))).(sn3_gen_def c d v0 i0 H2 H3)))))))
-(\lambda (v0: T).(\lambda (u2: T).(\lambda (u1: T).(\lambda (i0:
-nat).(\lambda (_: (subst0 i0 v0 u1 u2)).(\lambda (H3: ((\forall (c:
-C).(\forall (d: C).((getl i0 c (CHead d (Bind Abbr) v0)) \to ((sn3 c u1) \to
-(sn3 d v0))))))).(\lambda (t0: T).(\lambda (k: K).(\lambda (c: C).(\lambda
-(d: C).(\lambda (H4: (getl i0 c (CHead d (Bind Abbr) v0))).(\lambda (H5: (sn3
-c (THead k u1 t0))).(let H_y \def (sn3_gen_head k c u1 t0 H5) in (H3 c d H4
-H_y)))))))))))))) (\lambda (k: K).(\lambda (v0: T).(\lambda (t2: T).(\lambda
-(t1: T).(\lambda (i0: nat).(\lambda (H2: (subst0 (s k i0) v0 t1 t2)).(\lambda
-(H3: ((\forall (c: C).(\forall (d: C).((getl (s k i0) c (CHead d (Bind Abbr)
-v0)) \to ((sn3 c t1) \to (sn3 d v0))))))).(\lambda (u: T).(\lambda (c:
-C).(\lambda (d: C).(\lambda (H4: (getl i0 c (CHead d (Bind Abbr)
-v0))).(\lambda (H5: (sn3 c (THead k u t1))).(K_ind (\lambda (k0: K).((subst0
-(s k0 i0) v0 t1 t2) \to (((\forall (c0: C).(\forall (d0: C).((getl (s k0 i0)
-c0 (CHead d0 (Bind Abbr) v0)) \to ((sn3 c0 t1) \to (sn3 d0 v0)))))) \to ((sn3
-c (THead k0 u t1)) \to (sn3 d v0))))) (\lambda (b: B).(\lambda (_: (subst0 (s
-(Bind b) i0) v0 t1 t2)).(\lambda (H7: ((\forall (c0: C).(\forall (d0:
-C).((getl (s (Bind b) i0) c0 (CHead d0 (Bind Abbr) v0)) \to ((sn3 c0 t1) \to
-(sn3 d0 v0))))))).(\lambda (H8: (sn3 c (THead (Bind b) u t1))).(let H_x0 \def
-(sn3_gen_bind b c u t1 H8) in (let H9 \def H_x0 in (and_ind (sn3 c u) (sn3
-(CHead c (Bind b) u) t1) (sn3 d v0) (\lambda (_: (sn3 c u)).(\lambda (H11:
-(sn3 (CHead c (Bind b) u) t1)).(H7 (CHead c (Bind b) u) d (getl_clear_bind b
-(CHead c (Bind b) u) c u (clear_bind b c u) (CHead d (Bind Abbr) v0) i0 H4)
-H11))) H9))))))) (\lambda (f: F).(\lambda (_: (subst0 (s (Flat f) i0) v0 t1
-t2)).(\lambda (H7: ((\forall (c0: C).(\forall (d0: C).((getl (s (Flat f) i0)
-c0 (CHead d0 (Bind Abbr) v0)) \to ((sn3 c0 t1) \to (sn3 d0 v0))))))).(\lambda
-(H8: (sn3 c (THead (Flat f) u t1))).(let H_x0 \def (sn3_gen_flat f c u t1 H8)
-in (let H9 \def H_x0 in (and_ind (sn3 c u) (sn3 c t1) (sn3 d v0) (\lambda (_:
-(sn3 c u)).(\lambda (H11: (sn3 c t1)).(H7 c d H4 H11))) H9))))))) k H2 H3
-H5))))))))))))) (\lambda (v0: T).(\lambda (u1: T).(\lambda (u2: T).(\lambda
-(i0: nat).(\lambda (_: (subst0 i0 v0 u1 u2)).(\lambda (H3: ((\forall (c:
-C).(\forall (d: C).((getl i0 c (CHead d (Bind Abbr) v0)) \to ((sn3 c u1) \to
-(sn3 d v0))))))).(\lambda (k: K).(\lambda (t1: T).(\lambda (t2: T).(\lambda
-(_: (subst0 (s k i0) v0 t1 t2)).(\lambda (_: ((\forall (c: C).(\forall (d:
-C).((getl (s k i0) c (CHead d (Bind Abbr) v0)) \to ((sn3 c t1) \to (sn3 d
-v0))))))).(\lambda (c: C).(\lambda (d: C).(\lambda (H6: (getl i0 c (CHead d
-(Bind Abbr) v0))).(\lambda (H7: (sn3 c (THead k u1 t1))).(let H_y \def
-(sn3_gen_head k c u1 t1 H7) in (H3 c d H6 H_y))))))))))))))))) i v t x H1)))
-H0)))))).
-
projects / helm.git / blobdiff