proposition: Lemma simplify_eq_transport_nondep' {A} {B : A -> Type} {C : A -> Type} {x y : A} {e : eq x y} {z : &{ b : B x & C x}} {w : &{ b : B y & C y}} (P : @eq &{ _ : B y & C y } (e [ fun y => &{ b : B y & C y } ] # z) w -> Type) : (forall e1 : (eq (e # z.1) w.1), forall e2 : eq (e [fun x => C x] # z.2) w.2, P (distribute_sigma_eq_nondep' e1 e2)) -> (forall e' : eq (e # z) w, P e').
proof: Proof. intros. destruct e. simpl in *. destruct e'. specialize (X eq_refl eq_refl). simpl in X. exact X. Defined.
imports: Equations(Equations)