+#A #B #l1 elim l1 //
+ #a #tl #Hind #l2 #H1 #H2 @uniqueb_append
+ [@unique_map_inj //
+ |@Hind // @(andb_true_r … H1)
+ |#p #H3 cases (memb_map_to_exists … H3) #b *
+ #Hmemb #eqp <eqp @(not_to_not ? (memb ? a tl = true))
+ [2: @sym_not_eq @eqnot_to_noteq @sym_eq @(andb_true_l … H1)
+ |elim tl
+ [normalize //
+ |#a1 #tl1 #Hind2 #H4 cases (memb_append … H4) -H4 #H4
+ [cases (memb_map_to_exists … H4) #b1 * #memb1 #H destruct (H)
+ normalize >(\b (refl ? a)) //
+ |@orb_true_r2 @Hind2 @H4
+ ]
+ ]
+ ]
+ ]
+qed.