proposition: Lemma eq_rect_trans {A} {x y z : A} {P : A -> Type} (e : x = y) (e' : y = z) (p : P x) : rew (eq_trans e e') in p = rew e' in (rew e in p).
proof: Proof. destruct e'. simpl. reflexivity. Defined.
imports: Equations(Equations)