{n m l} : (n | m) -> (m | l) -> (n | l). Proof. intros [x p] [y q]. exists (y * x). lhs_V nrapply nat_mul_assoc. lhs nrapply (ap _ p). exact q. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.Classes