proposition: Lemma rew_in_sigma_nondep_inv {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') : (@eq_rect _ &(x & x') (fun x => C x.1 x.2) p _ (pack_sigma_eq_indep e e')) = q -> (e [ fun x => C x y' ] # (e' [fun lhs => C x lhs] # p) = q).
proof: Proof. destruct e, e'. simpl. trivial. Defined.
imports: Equations(Equations)