partial commit in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / grammar / lenv_append.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma
index c7d7ac9ca860277e4cb24d3101fa6def804baf81..0e8ec22fa318a36058df84b8e2bed0e54613d329 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma
@@ -23,6 +23,9 @@ let rec append L K on K ≝ match K with
 
 interpretation "append (local environment)" 'Append L1 L2 = (append L1 L2).
 
+definition l_appendable_sn: predicate (lenv→relation term) ≝ λR.
+                            ∀K,T1,T2. R K T1 T2 → ∀L. R (L @@ K) T1 T2.
+
 (* Basic properties *********************************************************)
 
 lemma append_atom_sn: ∀L. ⋆ @@ L = L.