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