proposition: Lemma simplify_eq_rect_trans {A} {B : A -> Type} {x y z : A} {e : eq x y} {e' : eq y z} {p : B x} {q : B z} (P : @eq (B z) (rew e' in (rew e in p)) q -> Type) : (forall e1 : (eq (rew (eq_trans e e') in p) q), P (eq_rect_trans e e' p [fun x => x = q] # e1)) -> (forall e'' : eq (rew e' in (rew e in p)) q, P e'').
proof: Proof. intros. destruct e. simpl in *. destruct e'. apply (X e''). Defined.
imports: Equations(Equations)