proposition: Lemma eq_rect_proj_dep {A} (x : A) {B : forall x' : A, eq x x' -> Type} {C : forall (x' : A) (e : eq x x'), B x' e -> Type} (y : A) (e : eq x y) (p : &{ b : B x eq_refl & C x eq_refl b }) : eq ((e [ fun x' (e : eq x x') => &{ b : B x' e & C x' e b } ] ## p).1) (e [ B ] ## p.1).
proof: Proof. destruct e. simpl. reflexivity. Defined.
imports: Equations(Equations)