(* *)
(**************************************************************************)
+include "ground/xoa/ex_1_2.ma".
include "static_2/notation/functions/snitem_2.ma".
include "static_2/notation/functions/snbind1_2.ma".
include "static_2/notation/functions/snbind2_3.ma".
rec definition append L K on K ≝ match K with
[ LAtom ⇒ L
-| LBind K I ⇒ (append L K).ⓘ{I}
+| LBind K I ⇒ (append L K).ⓘ[I]
].
interpretation "append (local environment)" 'plus L1 L2 = (append L1 L2).
// qed.
(* Basic_2A1: uses: append_pair *)
-lemma append_bind: ∀I,L,K. L+(K.ⓘ{I}) = (L+K).ⓘ{I}.
+lemma append_bind: ∀I,L,K. L+(K.ⓘ[I]) = (L+K).ⓘ[I].
// qed.
lemma append_atom_sn: ∀L. ⋆ + L = L.
#L1 #L2 #L3 elim L3 -L3 //
qed.
-lemma append_shift: ∀L,K,I. L+(ⓘ{I}.K) = (L.ⓘ{I})+K.
+lemma append_shift: ∀L,K,I. L+(ⓘ[I].K) = (L.ⓘ[I])+K.
#L #K #I <append_assoc //
qed.
#K #I >append_bind #H destruct
qed-.
-lemma append_inv_bind3_sn: ∀I0,L,L0,K. L0.ⓘ{I0} = L + K →
- ∨∨ ∧∧ L0.ⓘ{I0} = L & ⋆ = K
- | ∃∃K0. K = K0.ⓘ{I0} & L0 = L + K0.
+lemma append_inv_bind3_sn: ∀I0,L,L0,K. L0.ⓘ[I0] = L + K →
+ ∨∨ ∧∧ L0.ⓘ[I0] = L & ⋆ = K
+ | ∃∃K0. K = K0.ⓘ[I0] & L0 = L + K0.
#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-.
(* Basic_1: uses: chead_ctail *)
(* Basic_2A1: uses: lpair_ltail *)
-lemma lenv_case_tail: ∀L. L = ⋆ ∨ ∃∃K,I. L = ⓘ{I}.K.
+lemma lenv_case_tail: ∀L. L = ⋆ ∨ ∃∃K,I. L = ⓘ[I].K.
#L elim L -L /2 width=1 by or_introl/
#L #I * [2: * ] /3 width=3 by ex1_2_intro, or_intror/
qed-.