update in ground_2, static_2, basic_2

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / relocation / rtmap_eq.ma

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 8f0f5d0dfb46970fdc37ffe0a557e5152e81df03..8505c27c630594971c9cf9b577283dc2d566c696 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_eq.ma
@@ -12,27 +12,28 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground_2/notation/relations/funexteq_2.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: â\88\80f1,f2,g1,g2. eq f1 f2 â\86\92 â\86\91f1 = g1 â\86\92 â\86\91f2 = g2 → eq g1 g2
-| eq_next: â\88\80f1,f2,g1,g2. eq f1 f2 â\86\92 ⫯f1 = g1 â\86\92 ⫯f2 = g2 → eq g1 g2
+| eq_push: â\88\80f1,f2,g1,g2. eq f1 f2 â\86\92 ⫯f1 = g1 â\86\92 ⫯f2 = g2 → eq g1 g2
+| eq_next: â\88\80f1,f2,g1,g2. eq f1 f2 â\86\92 â\86\91f1 = g1 â\86\92 â\86\91f2 = 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 …) ≝
-                   â\88\80f1,f2. f1 â\89\97 f2 → R f1 f2.
+                   â\88\80f1,f2. f1 â\89¡ f2 → R f1 f2.
 
 definition eq_repl_back (R:predicate …) ≝
-                        â\88\80f1. R f1 â\86\92 â\88\80f2. f1 â\89\97 f2 → R f2.
+                        â\88\80f1. R f1 â\86\92 â\88\80f2. f1 â\89¡ f2 → R f2.
 
 definition eq_repl_fwd (R:predicate …) ≝
-                       â\88\80f1. R f1 â\86\92 â\88\80f2. f2 â\89\97 f1 → R f2.
+                       â\88\80f1. R f1 â\86\92 â\88\80f2. f2 â\89¡ f1 → R f2.
 
 (* Basic properties *********************************************************)
 
@@ -52,8 +53,8 @@ lemma eq_repl_sym: ∀R. eq_repl_back R → eq_repl_fwd R.
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma eq_inv_px: â\88\80g1,g2. g1 â\89\97 g2 â\86\92 â\88\80f1. â\86\91f1 = g1 →
-                 â\88\83â\88\83f2. f1 â\89\97 f2 & â\86\91f2 = g2.
+lemma eq_inv_px: â\88\80g1,g2. g1 â\89¡ g2 â\86\92 â\88\80f1. ⫯f1 = g1 →
+                 â\88\83â\88\83f2. f1 â\89¡ 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: â\88\80g1,g2. g1 â\89\97 g2 â\86\92 â\88\80f1. ⫯f1 = g1 →
-                 â\88\83â\88\83f2. f1 â\89\97 f2 & ⫯f2 = g2.
+lemma eq_inv_nx: â\88\80g1,g2. g1 â\89¡ g2 â\86\92 â\88\80f1. â\86\91f1 = g1 →
+                 â\88\83â\88\83f2. f1 â\89¡ f2 & â\86\91f2 = 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: â\88\80g1,g2. g1 â\89\97 g2 â\86\92 â\88\80f2. â\86\91f2 = g2 →
-                 â\88\83â\88\83f1. f1 â\89\97 f2 & â\86\91f1 = g1.
+lemma eq_inv_xp: â\88\80g1,g2. g1 â\89¡ g2 â\86\92 â\88\80f2. ⫯f2 = g2 →
+                 â\88\83â\88\83f1. f1 â\89¡ 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: â\88\80g1,g2. g1 â\89\97 g2 â\86\92 â\88\80f2. ⫯f2 = g2 →
-                 â\88\83â\88\83f1. f1 â\89\97 f2 & ⫯f1 = g1.
+lemma eq_inv_xn: â\88\80g1,g2. g1 â\89¡ g2 â\86\92 â\88\80f2. â\86\91f2 = g2 →
+                 â\88\83â\88\83f1. f1 â\89¡ f2 & â\86\91f1 = 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: â\88\80g1,g2. g1 â\89\97 g2 â\86\92 â\88\80f1,f2. â\86\91f1 = g1 â\86\92 â\86\91f2 = g2 â\86\92 f1 â\89\97 f2.
+lemma eq_inv_pp: â\88\80g1,g2. g1 â\89¡ g2 â\86\92 â\88\80f1,f2. ⫯f1 = g1 â\86\92 ⫯f2 = g2 â\86\92 f1 â\89¡ 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: â\88\80g1,g2. g1 â\89\97 g2 â\86\92 â\88\80f1,f2. ⫯f1 = g1 â\86\92 ⫯f2 = g2 â\86\92 f1 â\89\97 f2.
+lemma eq_inv_nn: â\88\80g1,g2. g1 â\89¡ g2 â\86\92 â\88\80f1,f2. â\86\91f1 = g1 â\86\92 â\86\91f2 = g2 â\86\92 f1 â\89¡ 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: â\88\80g1,g2. g1 â\89\97 g2 â\86\92 â\88\80f1,f2. â\86\91f1 = g1 â\86\92 ⫯f2 = g2 → ⊥.
+lemma eq_inv_pn: â\88\80g1,g2. g1 â\89¡ g2 â\86\92 â\88\80f1,f2. ⫯f1 = g1 â\86\92 â\86\91f2 = 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: â\88\80g1,g2. g1 â\89\97 g2 â\86\92 â\88\80f1,f2. ⫯f1 = g1 â\86\92 â\86\91f2 = g2 → ⊥.
+lemma eq_inv_np: â\88\80g1,g2. g1 â\89¡ g2 â\86\92 â\88\80f1,f2. â\86\91f1 = g1 â\86\92 ⫯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: â\88\80f1,f2. f1 â\89\97 f2 →
-                  (â\88\83â\88\83g1,g2. g1 â\89\97 g2 & â\86\91g1 = f1 & â\86\91g2 = f2) ∨
-                  â\88\83â\88\83g1,g2. g1 â\89\97 g2 & ⫯g1 = f1 & ⫯g2 = f2.
+lemma eq_inv_gen: â\88\80f1,f2. f1 â\89¡ f2 →
+                  (â\88\83â\88\83g1,g2. g1 â\89¡ g2 & ⫯g1 = f1 & ⫯g2 = f2) ∨
+                  â\88\83â\88\83g1,g2. g1 â\89¡ g2 & â\86\91g1 = f1 & â\86\91g2 = 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/
@@ -136,8 +137,8 @@ corec theorem eq_trans: Transitive … eq.
 /3 width=5 by eq_push, eq_next/
 qed-.
 
-theorem eq_canc_sn: â\88\80f2. eq_repl_back (λf. f â\89\97 f2).
+theorem eq_canc_sn: â\88\80f2. eq_repl_back (λf. f â\89¡ f2).
 /3 width=3 by eq_trans, eq_sym/ qed-.
 
-theorem eq_canc_dx: â\88\80f1. eq_repl_fwd (λf. f1 â\89\97 f).
+theorem eq_canc_dx: â\88\80f1. eq_repl_fwd (λf. f1 â\89¡ f).
 /3 width=3 by eq_trans, eq_sym/ qed-.