X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Frelocation%2Frtmap_eq.ma;h=8505c27c630594971c9cf9b577283dc2d566c696;hb=d8d00d6f6694155be5be486a8239f5953efe28b7;hp=44a83c7ff29fb59f5e3dd786ca9cc51cd88dd4db;hpb=91ab6965be539b7ed0f3208e1c1fffd17aa151f7;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_eq.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_eq.ma
index 44a83c7ff..8505c27c6 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_eq.ma
@@ -12,36 +12,37 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground_2/notation/relations/funexteq_2.ma".
-include "ground_2/relocation/nstream_lift.ma".
+include "ground_2/xoa/ex_3_2.ma".
+include "ground_2/notation/relations/ideq_2.ma".
+include "ground_2/relocation/rtmap.ma".
 
 (* RELOCATION MAP ***********************************************************)
 
 coinductive eq: relation rtmap ≝
-| eq_push: ∀f1,f2,g1,g2. eq f1 f2 → ↑f1 = g1 → ↑f2 = g2 → eq g1 g2
-| eq_next: ∀f1,f2,g1,g2. eq f1 f2 → ⫯f1 = g1 → ⫯f2 = g2 → eq g1 g2
+| eq_push: ∀f1,f2,g1,g2. eq f1 f2 → ⫯f1 = g1 → ⫯f2 = g2 → eq g1 g2
+| eq_next: ∀f1,f2,g1,g2. eq f1 f2 → ↑f1 = g1 → ↑f2 = g2 → eq g1 g2
 .
 
 interpretation "extensional equivalence (rtmap)"
-   'FunExtEq f1 f2 = (eq f1 f2).
+   'IdEq f1 f2 = (eq f1 f2).
 
 definition eq_repl (R:relation …) ≝
-                   ∀f1,f2. f1 ≗ f2 → R f1 f2.
+                   ∀f1,f2. f1 ≡ f2 → R f1 f2.
 
 definition eq_repl_back (R:predicate …) ≝
-                        ∀f1. R f1 → ∀f2. f1 ≗ f2 → R f2.
+                        ∀f1. R f1 → ∀f2. f1 ≡ f2 → R f2.
 
 definition eq_repl_fwd (R:predicate …) ≝
-                       ∀f1. R f1 → ∀f2. f2 ≗ f1 → R f2.
+                       ∀f1. R f1 → ∀f2. f2 ≡ f1 → R f2.
 
 (* Basic properties *********************************************************)
 
-let corec eq_refl: reflexive … eq ≝ ?.
+corec lemma eq_refl: reflexive … eq.
 #f cases (pn_split f) *
 #g #Hg [ @(eq_push … Hg Hg) | @(eq_next … Hg Hg) ] -Hg //
 qed.
 
-let corec eq_sym: symmetric … eq ≝ ?.
+corec lemma eq_sym: symmetric … eq.
 #f1 #f2 * -f1 -f2
 #f1 #f2 #g1 #g2 #Hf #H1 #H2
 [ @(eq_push … H2 H1) | @(eq_next … H2 H1) ] -g2 -g1 /2 width=1 by/
@@ -52,8 +53,8 @@ lemma eq_repl_sym: ∀R. eq_repl_back R → eq_repl_fwd R.
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma eq_inv_px: ∀g1,g2. g1 ≗ g2 → ∀f1. ↑f1 = g1 →
-                 ∃∃f2. f1 ≗ f2 & ↑f2 = g2.
+lemma eq_inv_px: ∀g1,g2. g1 ≡ g2 → ∀f1. ⫯f1 = g1 →
+                 ∃∃f2. f1 ≡ f2 & ⫯f2 = g2.
 #g1 #g2 * -g1 -g2
 #f1 #f2 #g1 #g2 #Hf * * -g1 -g2
 #x1 #H
@@ -62,8 +63,8 @@ lemma eq_inv_px: ∀g1,g2. g1 ≗ g2 → ∀f1. ↑f1 = g1 →
 ]
 qed-.
 
-lemma eq_inv_nx: ∀g1,g2. g1 ≗ g2 → ∀f1. ⫯f1 = g1 →
-                 ∃∃f2. f1 ≗ f2 & ⫯f2 = g2.
+lemma eq_inv_nx: ∀g1,g2. g1 ≡ g2 → ∀f1. ↑f1 = g1 →
+                 ∃∃f2. f1 ≡ f2 & ↑f2 = g2.
 #g1 #g2 * -g1 -g2
 #f1 #f2 #g1 #g2 #Hf * * -g1 -g2
 #x1 #H
@@ -72,8 +73,8 @@ lemma eq_inv_nx: ∀g1,g2. g1 ≗ g2 → ∀f1. ⫯f1 = g1 →
 ]
 qed-.
 
-lemma eq_inv_xp: ∀g1,g2. g1 ≗ g2 → ∀f2. ↑f2 = g2 →
-                 ∃∃f1. f1 ≗ f2 & ↑f1 = g1.
+lemma eq_inv_xp: ∀g1,g2. g1 ≡ g2 → ∀f2. ⫯f2 = g2 →
+                 ∃∃f1. f1 ≡ f2 & ⫯f1 = g1.
 #g1 #g2 * -g1 -g2
 #f1 #f2 #g1 #g2 #Hf * * -g1 -g2
 #x2 #H
@@ -82,8 +83,8 @@ lemma eq_inv_xp: ∀g1,g2. g1 ≗ g2 → ∀f2. ↑f2 = g2 →
 ]
 qed-.
 
-lemma eq_inv_xn: ∀g1,g2. g1 ≗ g2 → ∀f2. ⫯f2 = g2 →
-                 ∃∃f1. f1 ≗ f2 & ⫯f1 = g1.
+lemma eq_inv_xn: ∀g1,g2. g1 ≡ g2 → ∀f2. ↑f2 = g2 →
+                 ∃∃f1. f1 ≡ f2 & ↑f1 = g1.
 #g1 #g2 * -g1 -g2
 #f1 #f2 #g1 #g2 #Hf * * -g1 -g2
 #x2 #H
@@ -94,33 +95,33 @@ qed-.
 
 (* Advanced inversion lemmas ************************************************)
 
-lemma eq_inv_pp: ∀g1,g2. g1 ≗ g2 → ∀f1,f2. ↑f1 = g1 → ↑f2 = g2 → f1 ≗ f2.
+lemma eq_inv_pp: ∀g1,g2. g1 ≡ g2 → ∀f1,f2. ⫯f1 = g1 → ⫯f2 = g2 → f1 ≡ f2.
 #g1 #g2 #H #f1 #f2 #H1 elim (eq_inv_px … H … H1) -g1
 #x2 #Hx2 * -g2
 #H lapply (injective_push … H) -H //
 qed-.
 
-lemma eq_inv_nn: ∀g1,g2. g1 ≗ g2 → ∀f1,f2. ⫯f1 = g1 → ⫯f2 = g2 → f1 ≗ f2.
+lemma eq_inv_nn: ∀g1,g2. g1 ≡ g2 → ∀f1,f2. ↑f1 = g1 → ↑f2 = g2 → f1 ≡ f2.
 #g1 #g2 #H #f1 #f2 #H1 elim (eq_inv_nx … H … H1) -g1
 #x2 #Hx2 * -g2
 #H lapply (injective_next … H) -H //
 qed-.
 
-lemma eq_inv_pn: ∀g1,g2. g1 ≗ g2 → ∀f1,f2. ↑f1 = g1 → ⫯f2 = g2 → ⊥.
+lemma eq_inv_pn: ∀g1,g2. g1 ≡ g2 → ∀f1,f2. ⫯f1 = g1 → ↑f2 = g2 → ⊥.
 #g1 #g2 #H #f1 #f2 #H1 elim (eq_inv_px … H … H1) -g1
 #x2 #Hx2 * -g2
 #H elim (discr_next_push … H)
 qed-.
 
-lemma eq_inv_np: ∀g1,g2. g1 ≗ g2 → ∀f1,f2. ⫯f1 = g1 → ↑f2 = g2 → ⊥.
+lemma eq_inv_np: ∀g1,g2. g1 ≡ g2 → ∀f1,f2. ↑f1 = g1 → ⫯f2 = g2 → ⊥.
 #g1 #g2 #H #f1 #f2 #H1 elim (eq_inv_nx … H … H1) -g1
 #x2 #Hx2 * -g2
 #H elim (discr_push_next … H)
 qed-.
 
-lemma eq_inv_gen: ∀f1,f2. f1 ≗ f2 →
-                  (∃∃g1,g2. g1 ≗ g2 & ↑g1 = f1 & ↑g2 = f2) ∨
-                  ∃∃g1,g2. g1 ≗ g2 & ⫯g1 = f1 & ⫯g2 = f2.
+lemma eq_inv_gen: ∀f1,f2. f1 ≡ f2 →
+                  (∃∃g1,g2. g1 ≡ g2 & ⫯g1 = f1 & ⫯g2 = f2) ∨
+                  ∃∃g1,g2. g1 ≡ g2 & ↑g1 = f1 & ↑g2 = f2.
 #f1 elim (pn_split f1) * #g1 #H1 #f2 #Hf
 [ elim (eq_inv_px … Hf … H1) -Hf /3 width=5 by or_introl, ex3_2_intro/
 | elim (eq_inv_nx … Hf … H1) -Hf /3 width=5 by or_intror, ex3_2_intro/
@@ -129,15 +130,15 @@ qed-.
 
 (* Main properties **********************************************************)
 
-let corec eq_trans: Transitive … eq ≝ ?.
+corec theorem eq_trans: Transitive … eq.
 #f1 #f * -f1 -f
 #f1 #f #g1 #g #Hf1 #H1 #H #f2 #Hf2
 [ cases (eq_inv_px … Hf2 … H) | cases (eq_inv_nx … Hf2 … H) ] -g
 /3 width=5 by eq_push, eq_next/
 qed-.
 
-theorem eq_canc_sn: ∀f,f1,f2. f ≗ f1 → f ≗ f2 → f1 ≗ f2.
+theorem eq_canc_sn: ∀f2. eq_repl_back (λf. f ≡ f2).
 /3 width=3 by eq_trans, eq_sym/ qed-.
 
-theorem eq_canc_dx: ∀f,f1,f2. f1 ≗ f → f2 ≗ f → f1 ≗ f2.
+theorem eq_canc_dx: ∀f1. eq_repl_fwd (λf. f1 ≡ f).
 /3 width=3 by eq_trans, eq_sym/ qed-.