- lambda: some parts commented out, some refactoring

[helm.git] / matita / matita / contribs / lambda / labelled_hap_reduction.ma

diff --git a/matita/matita/contribs/lambda/labelled_hap_reduction.ma b/matita/matita/contribs/lambda/labelled_hap_reduction.ma
index 324ffdad993f03a07132d1cfc95f5f5391ed7b39..6d08b8c5c095c8a77097247c265ccda53e011769 100644 (file)
--- a/matita/matita/contribs/lambda/labelled_hap_reduction.ma
+++ b/matita/matita/contribs/lambda/labelled_hap_reduction.ma
@@ -20,27 +20,27 @@ include "labelled_sequential_reduction.ma".
          R. Kashima: "A proof of the Standization Theorem in λ-Calculus". Typescript note, (2000).
 *)
 inductive lhap1: ptr → relation term ≝
-| hap1_beta: â\88\80B,A. lhap1 (â\97\8a) (@B.ð\9d\9b\8c.A) ([â¬\90B]A)
+| hap1_beta: â\88\80B,A. lhap1 (â\97\8a) (@B.ð\9d\9b\8c.A) ([â\86\99B]A)
 | hap1_appl: ∀p,B,A1,A2. lhap1 p A1 A2 → lhap1 (dx::p) (@B.A1) (@B.A2)
 .
 
 interpretation "labelled 'hap' reduction"
    'HAp M p N = (lhap1 p M N).
 
-notation "hvbox( M break â\93\97â\87\80 [ term 46 p ] break term 46 N )"
+notation "hvbox( M break â\93\97â\86¦ [ term 46 p ] break term 46 N )"
    non associative with precedence 45
    for @{ 'HAp $M $p $N }.
 
-lemma lhap1_inv_nil: â\88\80p,M,N. M â\93\97â\87\80[p] N → ◊ = p →
-                     â\88\83â\88\83B,A. @B.ð\9d\9b\8c.A = M & [â¬\90B]A = N.
+lemma lhap1_inv_nil: â\88\80p,M,N. M â\93\97â\86¦[p] N → ◊ = p →
+                     â\88\83â\88\83B,A. @B.ð\9d\9b\8c.A = M & [â\86\99B]A = N.
 #p #M #N * -p -M -N
 [ #B #A #_ /2 width=4/
 | #p #B #A1 #A2 #_ #H destruct
 ]
 qed-.
 
-lemma lhap1_inv_cons: â\88\80p,M,N. M â\93\97â\87\80[p] N → ∀c,q. c::q = p →
-                      â\88\83â\88\83B,A1,A2. dx = c & A1 â\93\97â\87\80[q] A2 & @B.A1 = M & @B.A2 = N.
+lemma lhap1_inv_cons: â\88\80p,M,N. M â\93\97â\86¦[p] N → ∀c,q. c::q = p →
+                      â\88\83â\88\83B,A1,A2. dx = c & A1 â\93\97â\86¦[q] A2 & @B.A1 = M & @B.A2 = N.
 #p #M #N * -p -M -N
 [ #B #A #c #q #H destruct
 | #p #B #A1 #A2 #HA12 #c #q #H destruct /2 width=6/
@@ -69,7 +69,7 @@ lemma lhap1_dsubst: ∀p. dsubstable_dx (lhap1 p).
 #D2 #A #d >dsubst_dsubst_ge //
 qed.
 
-lemma head_lsred_lhap1: â\88\80p. in_head p â\86\92 â\88\80M,N. M â\87\80[p] N â\86\92 M â\93\97â\87\80[p] N.
+lemma head_lsred_lhap1: â\88\80p. in_head p â\86\92 â\88\80M,N. M â\86¦[p] N â\86\92 M â\93\97â\86¦[p] N.
 #p #H @(in_head_ind … H) -p
 [ #M #N #H elim (lsred_inv_nil … H ?) -H //
 | #p #_ #IHp #M #N #H
@@ -77,11 +77,11 @@ lemma head_lsred_lhap1: ∀p. in_head p → ∀M,N. M ⇀[p] N → M ⓗ⇀[p] N
 ]
 qed.
 
-lemma lhap1_inv_head: â\88\80p,M,N. M â\93\97â\87\80[p] N → in_head p.
+lemma lhap1_inv_head: â\88\80p,M,N. M â\93\97â\86¦[p] N → in_head p.
 #p #M #N #H elim H -p -M -N // /2 width=1/
 qed-.
 
-lemma lhap1_inv_lsred: â\88\80p,M,N. M â\93\97â\87\80[p] N â\86\92 M â\87\80[p] N.
+lemma lhap1_inv_lsred: â\88\80p,M,N. M â\93\97â\86¦[p] N â\86\92 M â\86¦[p] N.
 #p #M #N #H elim H -p -M -N // /2 width=1/
 qed-.