proposition: Lemma simplify_eq_rect_nested {A B} {C : A -> B -> Type} {x y : A} {e : x = y} {x' y' : B} {e' : x' = y'} (p : C x x') (q : C y y') (P : forall (x : (e [ fun x => C x y' ] # (e' [fun lhs => C x lhs] # p) = q)), Type) : (forall (e'' :(@eq_rect _ &(x & x') (fun x => C x.1 x.2) p _ (pack_sigma_eq_indep e e')) = q), P (@rew_in_sigma_nondep_inv _ _ _ x y e x' y' e' p q e'')) -> (forall e, P e).
proof: Proof. intros. destruct e, e'. simpl in *. apply X. Defined.
imports: Equations(Equations)