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