-(* cut (l1 = [〈a,false〉])
- [ cases l1'' in Hl1cons; // #y #ly #Hly
- >Hly in Hl1; cases l1' in Hl1bits;
- [ #_ normalize #Hfalse destruct (Hfalse)
- | #p #lp #Hl1bits normalize #Heq destruct (Heq)
- @False_ind lapply (Hl1bits 〈a,false〉 ?)
- [ cases lp in e0;
- [ normalize #Hfalse destruct (Hfalse)
- | #p0 #lp0 normalize in ⊢ (%→?); #Heq destruct (Heq)
- @memb_cons @memb_hd ]
- | >Ha normalize #Hfalse destruct (Hfalse) ]
- ]
- ] #Hl1a
- cut (l4 = [〈a0,false〉])
- [ generalize in match Hl4bits; cases l4' in Hl4;
- [ >Hl4cons #Hfalse #_
- lapply (inj_append_singleton_l1 ?? [] ?? Hfalse)
- cases (reverse ? l4'') normalize
- [ #Hfalse1 | #p0 #lp0 #Hfalse1 ] destruct (Hfalse1)
- | #p #lp
-
- cases l4'' in Hl4cons; // #y #ly #Hly
- >Hly in Hl4; cases l4' in Hl4bits;
- [ #_ >reverse_cons #Hfalse
- lapply (inj_append_singleton_l1 ?? [] ?? Hfalse)
- -Hfalse cases ly normalize
- [ #Hfalse | #p #Hp #Hfalse ] destruct (Hfalse)
-
- | #p #lp #Hl1bits normalize #Heq destruct (Heq)
- @False_ind lapply (Hl1bits 〈a,false〉 ?)
- [ cases lp in e0;
- [ normalize #Hfalse destruct (Hfalse)
- | #p0 #lp0 normalize in ⊢ (%→?); #Heq destruct (Heq)
- @memb_cons @memb_hd ]
- | >Ha normalize #Hfalse destruct (Hfalse) ]
- ]
- ] #Hl1a
-
- >Hla normalize #Hl1 destruct (Hl1) lapply (inj_append_ @False_ind
-
- cut (l1'' = [] ∧ l4'' = [])
- [ % [ >Hla in Hl1; normalize #Hl1 destruct (Hl1)
-
- cases l1'' in Hl1bits;
-
- [ #_ normalize #H *)