H14)))))) (pr0_subst0_fwd u0 t0 t i H7 x1 H12))))))) (wcpr0_getl (CHead c1 k
u) (CHead c2 k u) (wcpr0_comp c1 c2 H u u (pr0_refl u) k) i d u0 (Bind Abbr)
H9)))))))))))))) y t4 t3 H4))) H1) t5 H3))))))) t1 t2 H0)))))))).
H14)))))) (pr0_subst0_fwd u0 t0 t i H7 x1 H12))))))) (wcpr0_getl (CHead c1 k
u) (CHead c2 k u) (wcpr0_comp c1 c2 H u u (pr0_refl u) k) i d u0 (Bind Abbr)
H9)))))))))))))) y t4 t3 H4))) H1) t5 H3))))))) t1 t2 H0)))))))).