milestone update in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / static / feqg_feqg.ma

diff --git a/matita/matita/contribs/lambdadelta/static_2/static/feqg_feqg.ma b/matita/matita/contribs/lambdadelta/static_2/static/feqg_feqg.ma
index cb2b11ddd84761cd17fed859888847aa862e9cf7..7a3339a88fc2fc2efcbf6c8e45c627e8f9728d2f 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/static/feqg_feqg.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/feqg_feqg.ma
@@ -63,15 +63,22 @@ theorem feqg_canc_dx (S):
         ∀G2,L2,T2. ❪G2,L2,T2❫ ≛[S] ❪G,L,T❫ → ❪G1,L1,T1❫ ≛[S] ❪G2,L2,T2❫.
 /3 width=5 by feqg_trans, feqg_sym/ qed-.
 
-(* Main inversion lemmas with generic equivalence on terms ******************)
+lemma feqg_reqg_trans (S) (G2) (L) (T2):
+      reflexive … S → symmetric … S → Transitive … S →
+      ∀G1,L1,T1. ❪G1,L1,T1❫ ≛[S] ❪G2,L,T2❫ →
+      ∀L2. L ≛[S,T2] L2 → ❪G1,L1,T1❫ ≛[S] ❪G2,L2,T2❫.
+#S #G2 #L #T2 #H1S #H2S #H3S #G1 #L1 #T1 #H1 #L2 #HL2
+/4 width=5 by feqg_trans, feqg_intro_sn, teqg_refl/
+qed-.
 
-theorem feqg_tneqg_repl_dx (S):
-        reflexive … S → symmetric … S → Transitive … S →
-        ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≛[S] ❪G2,L2,T2❫ →
-        ∀U1,U2. ❪G1,L1,U1❫ ≛[S] ❪G2,L2,U2❫ →
-        (T2 ≛[S] U2 → ⊥) → (T1 ≛[S] U1 → ⊥).
-#S #H1S #H2S #H3S #G1 #G2 #L1 #L2 #T1 #T2 #HT #U1 #U2 #HU #HnTU2 #HTU1
-elim (feqg_inv_gen_sn … HT) -HT #_ #_ #HT
-elim (feqg_inv_gen_sn … HU) -HU #_ #_ #HU
-/3 width=5 by teqg_repl/
+(* Inversion lemmas with generic equivalence on terms ***********************)
+
+(* Basic_2A1: uses: feqg_tneqg_repl_dx *)
+lemma feqg_tneqg_trans (S) (G1) (G2) (L1) (L2) (T):
+      reflexive … S → symmetric … S → Transitive … S →
+      ∀T1. ❪G1,L1,T1❫ ≛[S] ❪G2,L2,T❫ →
+      ∀T2. (T ≛[S] T2 → ⊥) → (T1 ≛[S] T2 → ⊥).
+#S #G1 #G2 #L1 #L2 #T #H1S #H2S #H3S #T1 #H1 #T2 #HnT2 #HT12
+elim (feqg_inv_gen_sn … H1) -H1 #_ #_ #HnT1 -G1 -G2 -L1 -L2
+/3 width=3 by teqg_canc_sn/
 qed-.