proposition: Lemma simplify_eq_transport_nondep_dep {A} {B : Type} {C : A -> B -> Type} {x y : A} {e : eq x y} {z : &{ b : B & C x b}} {w : &{ b : B & C y b}} (P : @eq &{ b : B & C y b } (e [ fun y => &{ b : B & C y b } ] # z) w -> Type) : (forall (e1 : eq z.1 w.1) (e2 : eq (e1 [fun lhs => C y lhs] # (e [fun x => C x z.1] # z.2)) w.2), P (distribute_sigma_eq_nondep_dep 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)