#A #f #p elim p -p //
#p #IH @exteq_repl
/3 width=5 by compose_repl_fwd_dx, compose_repl_fwd_sn, exteq_canc_dx/
qed.
lemma piter_compose (A) (B) (f) (g) (h) (p):
#A #f #p elim p -p //
#p #IH @exteq_repl
/3 width=5 by compose_repl_fwd_dx, compose_repl_fwd_sn, exteq_canc_dx/
qed.
lemma piter_compose (A) (B) (f) (g) (h) (p):
#A #B #f #g #h #p elim p -p
[ #H @exteq_repl
/2 width=5 by compose_repl_fwd_sn, compose_repl_fwd_dx/
#A #B #f #g #h #p elim p -p
[ #H @exteq_repl
/2 width=5 by compose_repl_fwd_sn, compose_repl_fwd_dx/