(* This file was automatically generated: do not edit *********************)
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/spare".
-
-include "theory.ma".
-
-inductive sort: T \to Prop \def
-| sort_sort: \forall (n: nat).(sort (TSort n))
-| sort_abst: \forall (u: T).((sort u) \to (\forall (t: T).((sort t) \to (sort
-(THead (Bind Abst) u t))))).
-
-theorem sort_nf2:
- \forall (t: T).((sort t) \to (\forall (c: C).(nf2 c t)))
-\def
- \lambda (t: T).(\lambda (H: (sort t)).(sort_ind (\lambda (t0: T).(\forall
-(c: C).(nf2 c t0))) (\lambda (n: nat).(\lambda (c: C).(nf2_sort c n)))
-(\lambda (u: T).(\lambda (_: (sort u)).(\lambda (H1: ((\forall (c: C).(nf2 c
-u)))).(\lambda (t0: T).(\lambda (_: (sort t0)).(\lambda (H3: ((\forall (c:
-C).(nf2 c t0)))).(\lambda (c: C).(let H_y \def (H3 (CHead c (Bind Abst) u))
-in (nf2_abst_shift c u (H1 c) t0 H_y))))))))) t H)).
-
-theorem sort_pc3:
- \forall (t1: T).((sort t1) \to (\forall (t2: T).((sort t2) \to (\forall (c:
-C).((pc3 c t1 t2) \to (eq T t1 t2))))))
-\def
- \lambda (t1: T).(\lambda (H: (sort t1)).(sort_ind (\lambda (t: T).(\forall
-(t2: T).((sort t2) \to (\forall (c: C).((pc3 c t t2) \to (eq T t t2))))))
-(\lambda (n: nat).(\lambda (t2: T).(\lambda (H0: (sort t2)).(sort_ind
-(\lambda (t: T).(\forall (c: C).((pc3 c (TSort n) t) \to (eq T (TSort n)
-t)))) (\lambda (n0: nat).(\lambda (c: C).(\lambda (H1: (pc3 c (TSort n)
-(TSort n0))).(eq_ind nat n (\lambda (n1: nat).(eq T (TSort n) (TSort n1)))
-(refl_equal T (TSort n)) n0 (pc3_gen_sort c n n0 H1))))) (\lambda (u:
-T).(\lambda (_: (sort u)).(\lambda (_: ((\forall (c: C).((pc3 c (TSort n) u)
-\to (eq T (TSort n) u))))).(\lambda (t: T).(\lambda (_: (sort t)).(\lambda
-(_: ((\forall (c: C).((pc3 c (TSort n) t) \to (eq T (TSort n) t))))).(\lambda
-(c: C).(\lambda (H5: (pc3 c (TSort n) (THead (Bind Abst) u
-t))).(pc3_gen_sort_abst c u t n H5 (eq T (TSort n) (THead (Bind Abst) u
-t))))))))))) t2 H0)))) (\lambda (u: T).(\lambda (_: (sort u)).(\lambda (H1:
-((\forall (t2: T).((sort t2) \to (\forall (c: C).((pc3 c u t2) \to (eq T u
-t2))))))).(\lambda (t: T).(\lambda (_: (sort t)).(\lambda (H3: ((\forall (t2:
-T).((sort t2) \to (\forall (c: C).((pc3 c t t2) \to (eq T t
-t2))))))).(\lambda (t2: T).(\lambda (H4: (sort t2)).(sort_ind (\lambda (t0:
-T).(\forall (c: C).((pc3 c (THead (Bind Abst) u t) t0) \to (eq T (THead (Bind
-Abst) u t) t0)))) (\lambda (n: nat).(\lambda (c: C).(\lambda (H5: (pc3 c
-(THead (Bind Abst) u t) (TSort n))).(pc3_gen_sort_abst c u t n (pc3_s c
-(TSort n) (THead (Bind Abst) u t) H5) (eq T (THead (Bind Abst) u t) (TSort
-n)))))) (\lambda (u0: T).(\lambda (H5: (sort u0)).(\lambda (_: ((\forall (c:
-C).((pc3 c (THead (Bind Abst) u t) u0) \to (eq T (THead (Bind Abst) u t)
-u0))))).(\lambda (t0: T).(\lambda (H7: (sort t0)).(\lambda (_: ((\forall (c:
-C).((pc3 c (THead (Bind Abst) u t) t0) \to (eq T (THead (Bind Abst) u t)
-t0))))).(\lambda (c: C).(\lambda (H9: (pc3 c (THead (Bind Abst) u t) (THead
-(Bind Abst) u0 t0))).(and_ind (pc3 c u u0) (\forall (b: B).(\forall (u1:
-T).(pc3 (CHead c (Bind b) u1) t t0))) (eq T (THead (Bind Abst) u t) (THead
-(Bind Abst) u0 t0)) (\lambda (H10: (pc3 c u u0)).(\lambda (H11: ((\forall (b:
-B).(\forall (u1: T).(pc3 (CHead c (Bind b) u1) t t0))))).(let H_y \def (H11
-Abbr u) in (let H_y0 \def (H1 u0 H5 c H10) in (let H_y1 \def (H3 t0 H7 (CHead
-c (Bind Abbr) u) H_y) in (let H12 \def (eq_ind_r T t0 (\lambda (t3: T).(pc3
-(CHead c (Bind Abbr) u) t t3)) H_y t H_y1) in (let H13 \def (eq_ind_r T t0
-(\lambda (t3: T).(sort t3)) H7 t H_y1) in (eq_ind T t (\lambda (t3: T).(eq T
-(THead (Bind Abst) u t) (THead (Bind Abst) u0 t3))) (let H14 \def (eq_ind_r T
-u0 (\lambda (t3: T).(pc3 c u t3)) H10 u H_y0) in (let H15 \def (eq_ind_r T u0
-(\lambda (t3: T).(sort t3)) H5 u H_y0) in (eq_ind T u (\lambda (t3: T).(eq T
-(THead (Bind Abst) u t) (THead (Bind Abst) t3 t))) (refl_equal T (THead (Bind
-Abst) u t)) u0 H_y0))) t0 H_y1)))))))) (pc3_gen_abst c u u0 t t0 H9))))))))))
-t2 H4))))))))) t1 H)).
-
-theorem sort_correct:
- \forall (g: G).(\forall (t1: T).((sort t1) \to (\forall (c: C).(ex3 T
-(\lambda (t2: T).(tau0 g c t1 t2)) (\lambda (t2: T).(ty3 g c t1 t2)) (\lambda
-(t2: T).(sort t2))))))
-\def
- \lambda (g: G).(\lambda (t1: T).(\lambda (H: (sort t1)).(sort_ind (\lambda
-(t: T).(\forall (c: C).(ex3 T (\lambda (t2: T).(tau0 g c t t2)) (\lambda (t2:
-T).(ty3 g c t t2)) (\lambda (t2: T).(sort t2))))) (\lambda (n: nat).(\lambda
-(c: C).(ex3_intro T (\lambda (t2: T).(tau0 g c (TSort n) t2)) (\lambda (t2:
-T).(ty3 g c (TSort n) t2)) (\lambda (t2: T).(sort t2)) (TSort (next g n))
-(tau0_sort g c n) (ty3_sort g c n) (sort_sort (next g n))))) (\lambda (u:
-T).(\lambda (H0: (sort u)).(\lambda (H1: ((\forall (c: C).(ex3 T (\lambda
-(t2: T).(tau0 g c u t2)) (\lambda (t2: T).(ty3 g c u t2)) (\lambda (t2:
-T).(sort t2)))))).(\lambda (t: T).(\lambda (_: (sort t)).(\lambda (H3:
-((\forall (c: C).(ex3 T (\lambda (t2: T).(tau0 g c t t2)) (\lambda (t2:
-T).(ty3 g c t t2)) (\lambda (t2: T).(sort t2)))))).(\lambda (c: C).(let H_x
-\def (H1 c) in (let H4 \def H_x in (ex3_ind T (\lambda (t2: T).(tau0 g c u
-t2)) (\lambda (t2: T).(ty3 g c u t2)) (\lambda (t2: T).(sort t2)) (ex3 T
-(\lambda (t2: T).(tau0 g c (THead (Bind Abst) u t) t2)) (\lambda (t2: T).(ty3
-g c (THead (Bind Abst) u t) t2)) (\lambda (t2: T).(sort t2))) (\lambda (x0:
-T).(\lambda (_: (tau0 g c u x0)).(\lambda (H6: (ty3 g c u x0)).(\lambda (_:
-(sort x0)).(let H_x0 \def (H3 (CHead c (Bind Abst) u)) in (let H8 \def H_x0
-in (ex3_ind T (\lambda (t2: T).(tau0 g (CHead c (Bind Abst) u) t t2))
-(\lambda (t2: T).(ty3 g (CHead c (Bind Abst) u) t t2)) (\lambda (t2: T).(sort
-t2)) (ex3 T (\lambda (t2: T).(tau0 g c (THead (Bind Abst) u t) t2)) (\lambda
-(t2: T).(ty3 g c (THead (Bind Abst) u t) t2)) (\lambda (t2: T).(sort t2)))
-(\lambda (x1: T).(\lambda (H9: (tau0 g (CHead c (Bind Abst) u) t
-x1)).(\lambda (H10: (ty3 g (CHead c (Bind Abst) u) t x1)).(\lambda (H11:
-(sort x1)).(ex_ind T (\lambda (t0: T).(ty3 g (CHead c (Bind Abst) u) x1 t0))
-(ex3 T (\lambda (t2: T).(tau0 g c (THead (Bind Abst) u t) t2)) (\lambda (t2:
-T).(ty3 g c (THead (Bind Abst) u t) t2)) (\lambda (t2: T).(sort t2)))
-(\lambda (x: T).(\lambda (H12: (ty3 g (CHead c (Bind Abst) u) x1
-x)).(ex3_intro T (\lambda (t2: T).(tau0 g c (THead (Bind Abst) u t) t2))
-(\lambda (t2: T).(ty3 g c (THead (Bind Abst) u t) t2)) (\lambda (t2: T).(sort
-t2)) (THead (Bind Abst) u x1) (tau0_bind g Abst c u t x1 H9) (ty3_bind g c u
-x0 H6 Abst t x1 H10 x H12) (sort_abst u H0 x1 H11)))) (ty3_correct g (CHead c
-(Bind Abst) u) t x1 H10)))))) H8))))))) H4)))))))))) t1 H))).
+include "LambdaDelta-1/theory.ma".
+
+axiom pc3_gen_appls_sort_abst:
+ \forall (c: C).(\forall (vs: TList).(\forall (w: T).(\forall (u: T).(\forall
+(n: nat).((pc3 c (THeads (Flat Appl) vs (TSort n)) (THead (Bind Abst) w u))
+\to False)))))
+.
+
+axiom pc3_gen_appls_lref_abst:
+ \forall (c: C).(\forall (d: C).(\forall (v: T).(\forall (i: nat).((getl i c
+(CHead d (Bind Abst) v)) \to (\forall (vs: TList).(\forall (w: T).(\forall
+(u: T).((pc3 c (THeads (Flat Appl) vs (TLRef i)) (THead (Bind Abst) w u)) \to
+False))))))))
+.
+
+axiom pc3_gen_appls_lref_sort:
+ \forall (c: C).(\forall (d: C).(\forall (v: T).(\forall (i: nat).((getl i c
+(CHead d (Bind Abst) v)) \to (\forall (vs: TList).(\forall (ws:
+TList).(\forall (n: nat).((pc3 c (THeads (Flat Appl) vs (TLRef i)) (THeads
+(Flat Appl) ws (TSort n))) \to False))))))))
+.
projects / helm.git / blobdiff