X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Freduction%2Fdbfr.ma;h=7e4e6dbe367d9db1e1869e38f42e355e2ee66d58;hb=f31020f1ae14e28c246b6cd9cf91b5864f4f536a;hp=b9b7246332c8d36daf376af38637e96f84313319;hpb=7008128d354c6e998a87bc2febe9f86ea714869c;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr.ma
index b9b724633..7e4e6dbe3 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr.ma
@@ -34,3 +34,12 @@ definition dbfr (r): relation2 prototerm prototerm ≝
 interpretation
   "balanced focused reduction with delayed updating (prototerm)"
   'BlackRightArrowDBF t1 r t2 = (dbfr r t1 t2).
+
+(* Constructions with subset_equivalence ************************************)
+
+lemma dbfr_eq_trans (t) (t1) (t2) (r):
+      t1 ➡𝐝𝐛𝐟[r] t → t ⇔ t2 → t1 ➡𝐝𝐛𝐟[r] t2.
+#t #t1 #t2 #r
+* #p #b #q #m #n #Hr #Hb #Hm #Hn #Ht1 #Ht #Ht2
+/3 width=13 by subset_eq_trans, ex6_5_intro/
+qed-.