X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fsyntax%2Fpreterm.ma;h=6406d1dd7e50900f498b1832728315c5701e89e9;hb=306205b6853874cf485152222593b57249c6e7fa;hp=4d428e5ba8ae48488fa3702ef2cf7055718a0cc6;hpb=14e69a411768d60ce365547c1ffd88d9bef3cdc0;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm.ma
index 4d428e5ba..6406d1dd7 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm.ma
@@ -30,12 +30,12 @@ interpretation
 
 (* Basic inversions *********************************************************)
 
-lemma preterm_in_root_append_inv_structure_empty_dx (t) (p) (r):
-      p●r ϵ ▵t → t ϵ 𝐓 →  𝐞 = ⊗r → 𝐞 = r.
-#t #p #r #Hpr #Ht #Hr
-lapply (Ht p ?? Hpr ?)
+lemma preterm_in_root_append_inv_structure_empty_dx (t) (p) (q):
+      p●q ϵ ▵t → t ϵ 𝐓 → 𝐞 = ⊗q → 𝐞 = q.
+#t #p #q #Hpq #Ht #Hq
+lapply (Ht p ?? Hpq ?)
 [ <structure_append //
 | /2 width=2 by prototerm_in_root_append_des_sn/
-| /2 width=3 by eq_inv_list_append_dx_sn_refl/
+| /2 width=3 by eq_inv_list_append_dx_dx_refl/
 ]
 qed-.