>(lift_subst_up R S 1 0 (length ? D)) @(app … (lift Q (length ? D) 1));
[@Hind1 // |@Hind2 //]
|#G #P #Q #R #i #tjR #tjProd #Hind1 #Hind2
#G1 #D #A #l #Heq #tjA normalize @(abs … i);
[cut (∀n. S n = n +1); [//] #H <H
@(Hind1 G1 (P::D) … tjA) normalize //
>(lift_subst_up R S 1 0 (length ? D)) @(app … (lift Q (length ? D) 1));
[@Hind1 // |@Hind2 //]
|#G #P #Q #R #i #tjR #tjProd #Hind1 #Hind2
#G1 #D #A #l #Heq #tjA normalize @(abs … i);
[cut (∀n. S n = n +1); [//] #H <H
@(Hind1 G1 (P::D) … tjA) normalize //