proposition: Lemma simplify_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 }) q (P : (e [ fun x => &{ b : B & C x b } ] # p).1 = q -> Type) : (forall e' : p.1 = q, P (eq_trans2 (eq_rect_proj_nondep x y e p) e')) -> (forall x, P x).
proof: Proof. destruct e. simpl. intros. apply (X x0). Defined.
imports: Equations(Equations)