proposition: Lemma eq_rect_proj2 {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 }) : eq ((e [ fun x => &{ b : B x & C x b } ] # p).2) (e [ fun x e => C x (e #p).1 ] ## p.2).
proof: Proof. destruct e. simpl. reflexivity. Defined.
imports: Equations(Equations)