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