- | * #Hc' whd in ⊢ (%→?); #Helse2 %2 %
- [ generalize in match Hc'; generalize in match Hc;
- cases c'
- [ * [ #_ #Hfalse @False_ind @(absurd ?? Hfalse) %
- | #Hfalse @False_ind @(absurd ?? Hfalse) % ]
- |*: #_ #_ % ]
- | @(Helse2 … Hta)
+ | * #Hc' #Helse2 cases (Helse2 … Hta)
+ [ * #Hc'' #H1 % % [destruct (Hc'') % ]
+ #a #l1 #c0 #a0 #l2 #Hrs >Hrs in Hintape; #Hintape #Hl1
+ cases (H1 … Hl1 Hrs)
+ [ * #Htmp >Htmp -Htmp #Houtc % % // @Houtc
+ | * #Hneq #Houtc %2 %
+ [ @sym_not_eq //
+ | @Houtc ]
+ ]
+ | * #Hc'' whd in ⊢ (%→?); #Helse3 %2 %
+ [ generalize in match Hc''; generalize in match Hc'; generalize in match Hc;
+ cases c'
+ [ * [ #_ #Hfalse @False_ind @(absurd ?? Hfalse) %
+ | #Hfalse @False_ind @(absurd ?? Hfalse) % ]
+ | #_ #_ #Hfalse @False_ind @(absurd ?? Hfalse) %
+ |*: #_ #_ #_ % ]
+ | @(Helse3 … Hta)
+ ]