- #G1 #D #N #Heq #tjN (normalize in Hind1 ⊢ %)
- >(plus_n_O (length ? D)) in ⊢ (? ? ? ? (? ? % ?))
- >(subst_lemma R S N ? 0) (applyS app) /2/
+ #G1 #D #N #Heq #tjN normalize in Hind1 ⊢ %;
+ >(plus_n_O (length ? D)) in ⊢ (? ? ? ? (? ? % ?));
+ >(subst_lemma R S N ? 0) applyS app /2/