include "basic_2/notation/functions/snitem_2.ma".
include "basic_2/notation/functions/snbind1_2.ma".
include "basic_2/notation/functions/snbind2_3.ma".
include "basic_2/notation/functions/snitem_2.ma".
include "basic_2/notation/functions/snbind1_2.ma".
include "basic_2/notation/functions/snbind2_3.ma".
interpretation "local environment tail binding construction (generic)"
'SnItem I L = (append (LBind LAtom I) L).
interpretation "local environment tail binding construction (generic)"
'SnItem I L = (append (LBind LAtom I) L).
'SnAbst L T = (append (LBind LAtom (BPair Abst T)) L).
definition d_appendable_sn: predicate (lenv→relation term) ≝ λR.
'SnAbst L T = (append (LBind LAtom (BPair Abst T)) L).
definition d_appendable_sn: predicate (lenv→relation term) ≝ λR.
#L #K #I <append_assoc //
qed.
(* Basic inversion lemmas ***************************************************)
#L #K #I <append_assoc //
qed.
(* Basic inversion lemmas ***************************************************)
-lemma append_inv_bind3_sn: ∀I0,L,L0,K. L0.ⓘ{I0} = L @@ K →
+lemma append_inv_bind3_sn: ∀I0,L,L0,K. L0.ⓘ{I0} = L + K →
#I0 #L #L0 * /3 width=1 by or_introl, conj/
#K #I >append_bind #H destruct /3 width=3 by ex2_intro, or_intror/
qed-.
#I0 #L #L0 * /3 width=1 by or_introl, conj/
#K #I >append_bind #H destruct /3 width=3 by ex2_intro, or_intror/
qed-.
#K elim K -K //
#K #I #IH #L1 #L2 >append_bind #H
elim (destruct_lbind_lbind_aux … H) -H /2 width=1 by/ (**) (* destruct lemma needed *)
#K elim K -K //
#K #I #IH #L1 #L2 >append_bind #H
elim (destruct_lbind_lbind_aux … H) -H /2 width=1 by/ (**) (* destruct lemma needed *)