update in groud_2 and models

[helm.git] / matita / matita / contribs / lambdadelta / apps_2 / models / veq.ma

diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/veq.ma b/matita/matita/contribs/lambdadelta/apps_2/models/veq.ma
index 87a0800e75746a5481bc7e83207c9f159a64bed0..e784d3b7a8148c05e71034929822171fbfb9af43 100644 (file)
--- a/matita/matita/contribs/lambdadelta/apps_2/models/veq.ma
+++ b/matita/matita/contribs/lambdadelta/apps_2/models/veq.ma
@@ -32,10 +32,22 @@ lemma veq_repl (M): is_model M →
                     replace_2 … (veq M) (veq M) (veq M).
 /2 width=5 by mr/ qed-.
 
+lemma veq_sym (M): is_model M → symmetric … (veq M).
+/3 width=5 by veq_repl, veq_refl/ qed-.
+
+lemma veq_trans (M): is_model M → Transitive … (veq M).
+/3 width=5 by veq_repl, veq_refl/ qed-.
+
+(* Properties with extebsional equivalence **********************************)
+
 lemma ext_veq (M): is_model M →
                    ∀lv1,lv2. lv1 ≐ lv2 → lv1 ≗{M} lv2.
 /2 width=1 by mq/ qed.
 
+lemma veq_repl_exteq (M): is_model M →
+                          replace_2 … (veq M) (exteq …) (exteq …).
+/2 width=5 by mr/ qed-.
+
 lemma exteq_veq_trans (M): ∀lv1,lv. lv1 ≐ lv →
                            ∀lv2. lv ≗{M} lv2 → lv1 ≗ lv2.
 // qed-.