universary milestone in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / cprs.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma
index a8eb52ab50dc467bb522c133e4e26d7a3265e42e..638bcde72837fbd3f687dba24f256d403d542bb8 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma
@@ -52,12 +52,12 @@ lemma cprs_refl: ∀G,L,T. ⦃G, L⦄ ⊢ T ➡* T.
 
 lemma cprs_strap1: ∀G,L,T1,T,T2.
                    ⦃G, L⦄ ⊢ T1 ➡* T → ⦃G, L⦄ ⊢ T ➡ T2 → ⦃G, L⦄ ⊢ T1 ➡* T2.
-normalize /2 width=3 by step/ qed.
+normalize /2 width=3 by step/ qed-.
 
 (* Basic_1: was: pr3_step *)
 lemma cprs_strap2: ∀G,L,T1,T,T2.
                    ⦃G, L⦄ ⊢ T1 ➡ T → ⦃G, L⦄ ⊢ T ➡* T2 → ⦃G, L⦄ ⊢ T1 ➡* T2.
-normalize /2 width=3 by TC_strap/ qed.
+normalize /2 width=3 by TC_strap/ qed-.
 
 lemma lsubr_cprs_trans: ∀G. lsub_trans … (cprs G) lsubr.
 /3 width=5 by lsubr_cpr_trans, LTC_lsub_trans/
@@ -85,7 +85,7 @@ lemma cprs_flat_sn: ∀I,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ∀V1,V2. ⦃G,
 /3 width=3 by cprs_strap1, cpr_cprs, cpr_pair_sn, cpr_flat/
 qed.
 
-lemma cprs_zeta: â\88\80G,L,V,T1,T,T2. â\87§[0, 1] T2 ≡ T →
+lemma cprs_zeta: â\88\80G,L,V,T1,T,T2. â¬\86[0, 1] T2 ≡ T →
                  ⦃G, L.ⓓV⦄ ⊢ T1 ➡* T → ⦃G, L⦄ ⊢ +ⓓV.T1 ➡* T2.
 #G #L #V #T1 #T #T2 #HT2 #H @(cprs_ind_dx … H) -T1
 /3 width=3 by cprs_strap2, cpr_cprs, cpr_bind, cpr_zeta/
@@ -104,7 +104,7 @@ lemma cprs_beta_dx: ∀a,G,L,V1,V2,W1,W2,T1,T2.
 qed.
 
 lemma cprs_theta_dx: ∀a,G,L,V1,V,V2,W1,W2,T1,T2.
-                     â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡ V â\86\92 â\87§[0, 1] V ≡ V2 → ⦃G, L.ⓓW1⦄ ⊢ T1 ➡* T2 →
+                     â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡ V â\86\92 â¬\86[0, 1] V ≡ V2 → ⦃G, L.ⓓW1⦄ ⊢ T1 ➡* T2 →
                      ⦃G, L⦄ ⊢ W1 ➡ W2 → ⦃G, L⦄ ⊢ ⓐV1.ⓓ{a}W1.T1 ➡* ⓓ{a}W2.ⓐV2.T2.
 #a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 * -T2
 /4 width=9 by cprs_strap1, cpr_cprs, cprs_bind_dx, cprs_flat_dx, cpr_theta/
@@ -113,8 +113,8 @@ qed.
 (* Basic inversion lemmas ***************************************************)
 
 (* Basic_1: was: pr3_gen_sort *)
-lemma cprs_inv_sort1: ∀G,L,U2,k. ⦃G, L⦄ ⊢ ⋆k ➡* U2 → U2 = ⋆k.
-#G #L #U2 #k #H @(cprs_ind … H) -U2 //
+lemma cprs_inv_sort1: ∀G,L,U2,s. ⦃G, L⦄ ⊢ ⋆s ➡* U2 → U2 = ⋆s.
+#G #L #U2 #s #H @(cprs_ind … H) -U2 //
 #U2 #U #_ #HU2 #IHU2 destruct
 >(cpr_inv_sort1 … HU2) -HU2 //
 qed-.
@@ -122,7 +122,7 @@ qed-.
 (* Basic_1: was: pr3_gen_cast *)
 lemma cprs_inv_cast1: ∀G,L,W1,T1,U2. ⦃G, L⦄ ⊢ ⓝW1.T1 ➡* U2 → ⦃G, L⦄ ⊢ T1 ➡* U2 ∨
                       ∃∃W2,T2. ⦃G, L⦄ ⊢ W1 ➡* W2 & ⦃G, L⦄ ⊢ T1 ➡* T2 & U2 = ⓝW2.T2.
-#G #L #W1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5/
+#G #L #W1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5 by ex3_2_intro, or_intror/
 #U2 #U #_ #HU2 * /3 width=3 by cprs_strap1, or_introl/ *
 #W #T #HW1 #HT1 #H destruct
 elim (cpr_inv_cast1 … HU2) -HU2 /3 width=3 by cprs_strap1, or_introl/ *
@@ -140,5 +140,5 @@ qed-.
    pr1_head_1 pr1_head_2 pr1_comp
    clear_pr3_trans pr3_cflat pr3_gen_bind
    pr3_head_1 pr3_head_2 pr3_head_21 pr3_head_12
-   pr3_iso_appl_bind pr3_iso_applv_appl_bind pr3_iso_applv_bind
+   pr3_iso_appl_bind pr3_iso_appls_appl_bind pr3_iso_appls_bind
 *)