update in delayed-updating

[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / syntax / preterm.ma

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm.ma
index b7b90a4cf8f40e455866f8dd4c281c4252fbe935..4d428e5ba8ae48488fa3702ef2cf7055718a0cc6 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm.ma
@@ -27,3 +27,15 @@ definition structure_injective: predicate prototerm ≝
 interpretation
   "preterm (prototerm)"
   'ClassT = (structure_injective).
+
+(* 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 ?)
+[ <structure_append //
+| /2 width=2 by prototerm_in_root_append_des_sn/
+| /2 width=3 by eq_inv_list_append_dx_sn_refl/
+]
+qed-.