(* Basic constructions ******************************************************)
lemma list_append_empty_sn (A):
- â\88\80l2. l2 = â\92º ⨁{A} l2.
+ â\88\80l2. l2 = â\93\94 ⨁{A} l2.
// qed.
lemma list_append_lcons_sn (A):
(* Advanced constructions ***************************************************)
lemma list_append_empty_dx (A):
- â\88\80l1. l1 = l1 â¨\81{A} â\92º.
+ â\88\80l1. l1 = l1 â¨\81{A} â\93\94.
#A #l1 elim l1 -l1
[ <list_append_empty_sn //
| #hd #tl #IH <list_append_lcons_sn <IH //
]
]
qed.
+
+(* Basic inversions *********************************************************)
+
+lemma eq_inv_list_empty_append (A):
+ ∀l1,l2. ⓔ = l1⨁{A}l2 →
+ ∧∧ ⓔ = l1 & ⓔ = l2.
+#A *
+[ #l2 /2 width=1 by conj/
+| #a1 #l1 #l2 <list_append_lcons_sn #H destruct
+]
+qed-.
+
+lemma eq_inv_list_append_empty (A):
+ ∀l1,l2. l1⨁{A}l2 = ⓔ →
+ ∧∧ l1 = ⓔ & l2 = ⓔ.
+#A *
+[ #l2 /2 width=1 by conj/
+| #a1 #l1 #l2 <list_append_lcons_sn #H destruct
+]
+qed-.
+
+(* Advanced inversions ******************************************************)
+
+lemma eq_inv_list_append_dx_sn_refl (A) (l1) (l2):
+ l1 = l1⨁{A}l2 → ⓔ = l2.
+#A #l1 elim l1 -l1 [ // ]
+#a1 #l1 #IH #l2 <list_append_lcons_sn #H0 destruct -H0
+/2 width=1 by/
+qed-.
+
+(* Advanced eliminations ****************************************************)
+
+lemma list_ind_append_dx (A) (Q:predicate …):
+ Q (ⓔ{A}) →
+ (∀l1,l2. Q l1 -> Q (l1⨁l2)) →
+ ∀l. Q l.
+#A #Q #IH1 #IH2 * //
+#a #l >(list_append_empty_sn … (a⨮l))
+/2 width=1 by/
+qed-.