(* This file was automatically generated: do not edit *********************)
-include "pr3/props.ma".
+include "LambdaDelta-1/pr3/props.ma".
-include "wcpr0/getl.ma".
+include "LambdaDelta-1/wcpr0/getl.ma".
theorem pr3_wcpr0_t:
\forall (c1: C).(\forall (c2: C).((wcpr0 c2 c1) \to (\forall (t1:
T).(pr3_refl (CHead c0 k u1) t)) (\lambda (t0: T).(\lambda (t3: T).(\lambda
(H4: (pr2 (CHead c3 k u1) t3 t0)).(\lambda (t4: T).(\lambda (_: (pr3 (CHead
c3 k u1) t0 t4)).(\lambda (H6: (pr3 (CHead c0 k u1) t0 t4)).(pr3_t t0 t3
-(CHead c0 k u1) (let H7 \def (match H4 in pr2 return (\lambda (c: C).(\lambda
-(t: T).(\lambda (t5: T).(\lambda (_: (pr2 c t t5)).((eq C c (CHead c3 k u1))
-\to ((eq T t t3) \to ((eq T t5 t0) \to (pr3 (CHead c0 k u1) t3 t0))))))))
-with [(pr2_free c t5 t6 H7) \Rightarrow (\lambda (H8: (eq C c (CHead c3 k
-u1))).(\lambda (H9: (eq T t5 t3)).(\lambda (H10: (eq T t6 t0)).(eq_ind C
-(CHead c3 k u1) (\lambda (_: C).((eq T t5 t3) \to ((eq T t6 t0) \to ((pr0 t5
-t6) \to (pr3 (CHead c0 k u1) t3 t0))))) (\lambda (H11: (eq T t5 t3)).(eq_ind
-T t3 (\lambda (t: T).((eq T t6 t0) \to ((pr0 t t6) \to (pr3 (CHead c0 k u1)
-t3 t0)))) (\lambda (H12: (eq T t6 t0)).(eq_ind T t0 (\lambda (t: T).((pr0 t3
-t) \to (pr3 (CHead c0 k u1) t3 t0))) (\lambda (H13: (pr0 t3 t0)).(pr3_pr2
-(CHead c0 k u1) t3 t0 (pr2_free (CHead c0 k u1) t3 t0 H13))) t6 (sym_eq T t6
-t0 H12))) t5 (sym_eq T t5 t3 H11))) c (sym_eq C c (CHead c3 k u1) H8) H9 H10
-H7)))) | (pr2_delta c d u i H7 t5 t6 H8 t H9) \Rightarrow (\lambda (H10: (eq
-C c (CHead c3 k u1))).(\lambda (H11: (eq T t5 t3)).(\lambda (H12: (eq T t
-t0)).(eq_ind C (CHead c3 k u1) (\lambda (c4: C).((eq T t5 t3) \to ((eq T t
-t0) \to ((getl i c4 (CHead d (Bind Abbr) u)) \to ((pr0 t5 t6) \to ((subst0 i
-u t6 t) \to (pr3 (CHead c0 k u1) t3 t0))))))) (\lambda (H13: (eq T t5
-t3)).(eq_ind T t3 (\lambda (t7: T).((eq T t t0) \to ((getl i (CHead c3 k u1)
-(CHead d (Bind Abbr) u)) \to ((pr0 t7 t6) \to ((subst0 i u t6 t) \to (pr3
-(CHead c0 k u1) t3 t0)))))) (\lambda (H14: (eq T t t0)).(eq_ind T t0 (\lambda
-(t7: T).((getl i (CHead c3 k u1) (CHead d (Bind Abbr) u)) \to ((pr0 t3 t6)
-\to ((subst0 i u t6 t7) \to (pr3 (CHead c0 k u1) t3 t0))))) (\lambda (H15:
-(getl i (CHead c3 k u1) (CHead d (Bind Abbr) u))).(\lambda (H16: (pr0 t3
-t6)).(\lambda (H17: (subst0 i u t6 t0)).(ex3_2_ind C T (\lambda (e2:
+(CHead c0 k u1) (insert_eq C (CHead c3 k u1) (\lambda (c: C).(pr2 c t3 t0))
+(\lambda (_: C).(pr3 (CHead c0 k u1) t3 t0)) (\lambda (y: C).(\lambda (H7:
+(pr2 y t3 t0)).(pr2_ind (\lambda (c: C).(\lambda (t: T).(\lambda (t5: T).((eq
+C c (CHead c3 k u1)) \to (pr3 (CHead c0 k u1) t t5))))) (\lambda (c:
+C).(\lambda (t5: T).(\lambda (t6: T).(\lambda (H8: (pr0 t5 t6)).(\lambda (_:
+(eq C c (CHead c3 k u1))).(pr3_pr2 (CHead c0 k u1) t5 t6 (pr2_free (CHead c0
+k u1) t5 t6 H8))))))) (\lambda (c: C).(\lambda (d: C).(\lambda (u:
+T).(\lambda (i: nat).(\lambda (H8: (getl i c (CHead d (Bind Abbr)
+u))).(\lambda (t5: T).(\lambda (t6: T).(\lambda (H9: (pr0 t5 t6)).(\lambda
+(t: T).(\lambda (H10: (subst0 i u t6 t)).(\lambda (H11: (eq C c (CHead c3 k
+u1))).(let H12 \def (eq_ind C c (\lambda (c4: C).(getl i c4 (CHead d (Bind
+Abbr) u))) H8 (CHead c3 k u1) H11) in (ex3_2_ind C T (\lambda (e2:
C).(\lambda (u3: T).(getl i (CHead c0 k u1) (CHead e2 (Bind Abbr) u3))))
(\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 d))) (\lambda (_: C).(\lambda (u3:
-T).(pr0 u3 u))) (pr3 (CHead c0 k u1) t3 t0) (\lambda (x0: C).(\lambda (x1:
-T).(\lambda (H18: (getl i (CHead c0 k u1) (CHead x0 (Bind Abbr)
-x1))).(\lambda (_: (wcpr0 x0 d)).(\lambda (H20: (pr0 x1 u)).(ex2_ind T
-(\lambda (t7: T).(subst0 i x1 t6 t7)) (\lambda (t7: T).(pr0 t7 t0)) (pr3
-(CHead c0 k u1) t3 t0) (\lambda (x: T).(\lambda (H21: (subst0 i x1 t6
-x)).(\lambda (H22: (pr0 x t0)).(pr3_sing (CHead c0 k u1) x t3 (pr2_delta
-(CHead c0 k u1) x0 x1 i H18 t3 t6 H16 x H21) t0 (pr3_pr2 (CHead c0 k u1) x t0
-(pr2_free (CHead c0 k u1) x t0 H22)))))) (pr0_subst0_back u t6 t0 i H17 x1
-H20))))))) (wcpr0_getl_back (CHead c3 k u1) (CHead c0 k u1) (wcpr0_comp c0 c3
-H0 u1 u1 (pr0_refl u1) k) i d u (Bind Abbr) H15))))) t (sym_eq T t t0 H14)))
-t5 (sym_eq T t5 t3 H13))) c (sym_eq C c (CHead c3 k u1) H10) H11 H12 H7 H8
-H9))))]) in (H7 (refl_equal C (CHead c3 k u1)) (refl_equal T t3) (refl_equal
-T t0))) t4 H6))))))) t1 t2 (pr3_pr2_pr3_t c3 u2 t1 t2 k H3 u1 (pr2_free c3 u1
-u2 H2)))))))))))))) c2 c1 H))).
+T).(pr0 u3 u))) (pr3 (CHead c0 k u1) t5 t) (\lambda (x0: C).(\lambda (x1:
+T).(\lambda (H13: (getl i (CHead c0 k u1) (CHead x0 (Bind Abbr)
+x1))).(\lambda (_: (wcpr0 x0 d)).(\lambda (H15: (pr0 x1 u)).(ex2_ind T
+(\lambda (t7: T).(subst0 i x1 t6 t7)) (\lambda (t7: T).(pr0 t7 t)) (pr3
+(CHead c0 k u1) t5 t) (\lambda (x: T).(\lambda (H16: (subst0 i x1 t6
+x)).(\lambda (H17: (pr0 x t)).(pr3_sing (CHead c0 k u1) x t5 (pr2_delta
+(CHead c0 k u1) x0 x1 i H13 t5 t6 H9 x H16) t (pr3_pr2 (CHead c0 k u1) x t
+(pr2_free (CHead c0 k u1) x t H17)))))) (pr0_subst0_back u t6 t i H10 x1
+H15))))))) (wcpr0_getl_back (CHead c3 k u1) (CHead c0 k u1) (wcpr0_comp c0 c3
+H0 u1 u1 (pr0_refl u1) k) i d u (Bind Abbr) H12)))))))))))))) y t3 t0 H7)))
+H4) t4 H6))))))) t1 t2 (pr3_pr2_pr3_t c3 u2 t1 t2 k H3 u1 (pr2_free c3 u1 u2
+H2)))))))))))))) c2 c1 H))).
projects / helm.git / blobdiff