X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fapps_2%2Fmodels%2Fveq.ma;h=e784d3b7a8148c05e71034929822171fbfb9af43;hp=87a0800e75746a5481bc7e83207c9f159a64bed0;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hpb=f86ab1580e0bab7f8cada3cc7ffdf80f40e3de9a

diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/veq.ma b/matita/matita/contribs/lambdadelta/apps_2/models/veq.ma
index 87a0800e7..e784d3b7a 100644
--- 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-.