+#A #l1 #l2 #l3 generalize in match l1; generalize in match l2; elim l3
+ [normalize #l1 #l2 #l4 #a #H #_ @(ex_intro … []) @(ex_intro … l2) /2/
+ |#b #tl #Hind #l1 #l2 #l4 #a cases l2
+ [normalize #Heq destruct >(\b (refl … b)) normalize #Hfalse destruct
+ |#c #tl2 whd in ⊢ ((??%%)→?); #Heq destruct #Hmema
+ cases (Hind l1 tl2 l4 a ??)
+ [#l5 * #l6 * #eql #eql4
+ @(ex_intro … (b::l5)) @(ex_intro … l6) % /2/
+ |@e0
+ |cases (true_or_false (memb ? a tl)) [2://]
+ #H @False_ind @(absurd ?? not_eq_true_false)
+ <Hmema @sym_eq @memb_cons //
+ ]
+ ]
+ ]
+qed.
+