- cut (∃l2.xs = x2::xs2@ci::l2)
- [lapply Hnotend -Hnotend lapply Hxs elim xs in Hxs;
- [ normalize #H1 #_ destruct (H1)
- >(Hnotendxs2 ? (memb_hd …)) in Hend; #H1 destruct (H1)
- | #x3 #xs3 #IH normalize in ⊢ (%→?); #Hxs3 destruct (Hxs3)
- #Hnotend
-
- @daemon] * #l2 #Hxs'
+ cut (∃l2.xs = (x2::xs2)@ci::l2)
+ [lapply Hnotendxs2
+ lapply Hnotend -Hnotend lapply Hxs
+ >(?:x2::xs2@ci::tl1 = (x2::xs2)@ci::tl1) [|%]
+ lapply (x2::xs2) elim xs
+ [ *
+ [ normalize in ⊢ (%→?); #H1 destruct (H1)
+ >Hendci in Hend; #Hend destruct (Hend)
+ | #x3 #xs3 normalize in ⊢ (%→?); #H1 destruct (H1)
+ #_ #Hnotendx3 >(Hnotendx3 ? (memb_hd …)) in Hend;
+ #Hend destruct (Hend)
+ ]
+ | #x3 #xs3 #IHin *
+ [ normalize in ⊢ (%→?); #Hxs3 destruct (Hxs3) #_ #_
+ %{xs3} %
+ | #x4 #xs4 normalize in ⊢ (%→?); #Hxs3xs4 #Hnotend
+ #Hnotendxs4 destruct (Hxs3xs4) cases (IHin ? e0 ??)
+ [ #l0 #Hxs3 >Hxs3 %{l0} %
+ | #c0 #Hc0 @Hnotend cases (orb_true_l … Hc0) -Hc0 #Hc0
+ [ >(\P Hc0) @memb_hd
+ | @memb_cons @memb_cons @Hc0 ]
+ | #c0 #Hc0 @Hnotendxs4 @memb_cons //
+ ]
+ ]
+ ]
+ ] * #l2 #Hxs'