+lemma memb_unique_append: ∀S,a,l1,l2.
+ \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a (\ 5a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"\ 6unique_append\ 5/a\ 6 S l1 l2) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a l1\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
+#S #a #l1 elim l1 normalize [#l2 #H %2 //]
+#b #tl #Hind #l2 cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 … (a\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6=b)) #Hab >Hab normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/bool/orb_true_l.def(2)"\ 6orb_true_l\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+cases (\ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S b (\ 5a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"\ 6unique_append\ 5/a\ 6 S tl l2)) normalize
+ [@Hind | >Hab normalize @Hind]
+qed.
+