include "static_2/notation/functions/snitem_2.ma".
include "static_2/notation/functions/snbind1_2.ma".
include "static_2/notation/functions/snbind2_3.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".
-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-.
#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-.
#L elim L -L /2 width=1 by or_introl/
#L #I * [2: * ] /3 width=3 by ex1_2_intro, or_intror/
qed-.
#L elim L -L /2 width=1 by or_introl/
#L #I * [2: * ] /3 width=3 by ex1_2_intro, or_intror/
qed-.