- #Hta lapply (proj2 … Htb … Hta) -Htb -Hta cases rs
- [whd in ⊢ ((???%)→?); #Htb >Htb in Htc; #Htc
- lapply (proj1 ?? Htc (refl …)) -Htc #Htc <Htc in Houtc;
- |#a #l1 #x0 #a0 #l2 #_ #Hrs @False_ind
+ #Hta lapply (proj2 … Htb … Hta) -Htb -Hta cases rs in Hdec;
+ [#_ whd in ⊢ ((???%)→?); #Htb >Htb in Htc; #Htc
+ lapply (proj1 ?? Htc (refl …)) -Htc #Htc <Htc in Houtc1; #Houtc1
+ normalize in ⊢ (???%→?); #Hl1 destruct(Hl1) @(Houtc1 (refl …))
+ |#r0 #rs0 #Hdec whd in ⊢ ((???%)→?); #Htb >Htb in Htc; #Htc
+ >reverse_cons >reverse_cons #Hl1
+ cases (proj2 ?? Htc … (refl …))
+ [* >(Hdec …) [ #Hfalse destruct(Hfalse) ] @memb_hd
+ |* #_ -Htc #Htc cut (∃l2.l1 = l2@[〈x,true〉])
+ [generalize in match Hl1; -Hl1 <(reverse_reverse … l1)
+ cases (reverse ? l1)
+ [#Hl1 cut ([a]=〈x,true〉::r0::rs0)
+ [ <(reverse_reverse … (〈x,true〉::r0::rs0))
+ >reverse_cons >reverse_cons <Hl1 %
+ | #Hfalse destruct(Hfalse)]
+ |#a0 #l10 >reverse_cons #Heq
+ lapply (append_l2_injective_r ? (a::reverse ? l10) ???? Heq) //
+ #Ha0 destruct(Ha0) /2/ ]
+ |* #l2 #Hl2 >Hl2 in Hl1; #Hl1
+ lapply (append_l1_injective_r ? (a::l2) … Hl1) // -Hl1 #Hl1
+ >reverse_cons in Htc; #Htc lapply (Htc … (sym_eq … Hl1))
+ [ #x0 #Hmemb @Hdec @memb_cons @Hmemb ]
+ -Htc #Htc >Htc in Houtc1; #Houtc1 >associative_append @Houtc1 %
+ ]
+ ]
+ ]
+ |#a #l1 #x0 #a0
+ #l2 #_ #Hrs @False_ind