(leq g a1 a2)).(\lambda (d1: C).(\lambda (is: PList).(\lambda (H3: (drop1 is
d1 c)).(\lambda (c2: C).(\lambda (H4: (csubc g d1 c2)).(sc3_repl g a1 c2
(lift1 is t0) (H1 d1 is H3 c2 H4) a2 H2))))))))))))) c1 t a H))))).
(leq g a1 a2)).(\lambda (d1: C).(\lambda (is: PList).(\lambda (H3: (drop1 is
d1 c)).(\lambda (c2: C).(\lambda (H4: (csubc g d1 c2)).(sc3_repl g a1 c2
(lift1 is t0) (H1 d1 is H3 c2 H4) a2 H2))))))))))))) c1 t a H))))).