- bug fix in the connection between global and restricted big-tree

[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..24e08d1516e1e5712d87a999c48f5fc03984ef40 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.
@@ -48,7 +51,7 @@ lemma append_inj_sn: ∀K1,K2,L1,L2. L1 @@ K1 = L2 @@ K2 → |K1| = |K2| →
   [ #L1 #L2 #_ <plus_n_Sm #H destruct
   | #K2 #I2 #V2 #L1 #L2 #H1 #H2
     elim (destruct_lpair_lpair … H1) -H1 #H1 #H3 #H4 destruct (**) (* destruct lemma needed *)
-    elim (IH … H1 ?) -IH -H1 // -H2 /2 width=1/
+    elim (IH … H1) -IH -H1 // -H2 /2 width=1/
   ]
 ]
 qed-.
@@ -67,19 +70,19 @@ lemma append_inj_dx: ∀K1,K2,L1,L2. L1 @@ K1 = L2 @@ K2 → |L1| = |L2| →
     elim (plus_xySz_x_false … (sym_eq … H))
   | #K2 #I2 #V2 #L1 #L2 #H1 #H2
     elim (destruct_lpair_lpair … H1) -H1 #H1 #H3 #H4 destruct (**) (* destruct lemma needed *)
-    elim (IH … H1 ?) -IH -H1 // -H2 /2 width=1/
+    elim (IH … H1) -IH -H1 // -H2 /2 width=1/
   ]
 ]
 qed-.
 
 lemma append_inv_refl_dx: ∀L,K. L @@ K = L → K = ⋆.
 #L #K #H
-elim (append_inj_dx … (⋆) … H ?) //
+elim (append_inj_dx … (⋆) … H) //
 qed-.
 
 lemma append_inv_pair_dx: ∀I,L,K,V. L @@ K = L.ⓑ{I}V → K = ⋆.ⓑ{I}V.
 #I #L #K #V #H
-elim (append_inj_dx … (⋆.ⓑ{I}V) … H ?) //
+elim (append_inj_dx … (⋆.ⓑ{I}V) … H) //
 qed-.
 
 lemma length_inv_pos_dx_append: ∀d,L. |L| = d + 1 →
@@ -123,7 +126,7 @@ lemma length_inv_pos_sn_append: ∀d,L. 1 + d = |L| →
   @(ex2_3_intro … (⋆)) // (**) (* explicit constructor *)
 | #d #IHd #L #H elim (length_inv_pos_sn … H) -H #I #K #V #H1 #H2 destruct
   >H1 in IHd; -H1 #IHd
-  elim (IHd K ?) -IHd // #J #L #W #H1 #H2 destruct
+  elim (IHd K) -IHd // #J #L #W #H1 #H2 destruct
   @(ex2_3_intro … (L.ⓑ{I}V)) // (**) (* explicit constructor *)
   >append_length /2 width=1/
 ]