- * #tb * whd in ⊢ (%→?); #Htb cases (Htb … Hta) -Hta
- [* >Hc #Htemp destruct (Htemp) ]
- * #_ #Htc lapply (Htc [ ] 〈grid,false〉 ? (refl ??) (refl …) Hl1)
- whd in ⊢ ((???(??%%%))→?); -Htc #Htc
- * #td * whd in ⊢ (%→?); #Htd lapply (Htd … Htc) -Htc -Htd
- whd in ⊢ ((???(??%%%))→?); #Htd
- whd in ⊢ (%→?); #Houtc lapply (Houtc … Htd) -Houtc #Houtc
+ * #tb * whd in ⊢ (%→?); * #_ #Htb cases (Htb … Hta) -Htb -Hta #_
+ (* [* >Hc #Htemp destruct (Htemp) ] *)
+ #Htb cases (Htb … Hc) -Htb #Htb #_
+ lapply (Htb [ ] 〈grid,false〉 ? (refl ??) (refl …) Hl1)
+ whd in ⊢ ((???(??%%%))→?); -Htb #Htb
+ * #tc * whd in ⊢ (%→?); * #_ #Htc lapply (Htc … Htb) -Htb -Htc
+ whd in ⊢ ((???(??%%%))→?); #Htc
+ whd in ⊢ (%→?); * #Houtc #_ lapply (Houtc … Htc) -Houtc #Houtc