milestone update in basic_2

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

diff --git a/matita/matita/contribs/lambdadelta/static_2/static/feqg.ma b/matita/matita/contribs/lambdadelta/static_2/static/feqg.ma
index 39cba31e932f8b7d90d1a14e7a79ce6cbf80c167..378e52d910bdda81d19ddc4f63e77e70ef015383 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/static/feqg.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/feqg.ma
@@ -51,6 +51,27 @@ lemma feqg_inv_gen_dx (S):
 /3 width=6 by teqg_reqg_conf_sn, and3_intro/
 qed-.
 
+(* Basic forward lemmas *****************************************************)
+
+lemma feqg_fwd_teqg (S):
+      ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≛[S] ❪G2,L2,T2❫ → T1 ≛[S] T2.
+#S #G1 #G2 #L1 #L2 #T1 #T2 #H
+elim (feqg_inv_gen_sn … H) -H //
+qed-.
+
+lemma feqg_fwd_reqg_sn (S):
+      ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≛[S] ❪G2,L2,T2❫ → L1 ≛[S,T1] L2.
+#S #G1 #G2 #L1 #L2 #T1 #T2 #H
+elim (feqg_inv_gen_sn … H) -H //
+qed-.
+
+lemma feqg_fwd_reqg_dx (S):
+      reflexive … S →
+      ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≛[S] ❪G2,L2,T2❫ → L1 ≛[S,T2] L2.
+#S #HS #G1 #G2 #L1 #L2 #T1 #T2 #H
+elim (feqg_inv_gen_dx … H) -H //
+qed-.
+
 (* Basic_2A1: removed theorems 6:
               fleq_refl fleq_sym fleq_inv_gen
               fleq_trans fleq_canc_sn fleq_canc_dx