proposition: Lemma apply_equiv_codom {A} {B B' : A -> Type} (e : forall x, Equiv (B x) (B' x)) : (forall x : A, B x) <~> forall x : A, B' x.
proof: Proof. intros. unshelve refine {| equiv f := fun x => e x (f x) |}. unshelve refine {| equiv_inv f := fun x => (e x)^-1 (f x) |}. red; intros. extensionality y. apply inv_equiv_equiv. intro. extensionality y. apply equiv_inv_equiv. intros. apply axiom_triangle. Defined.
imports: Equations Utf8 DepElimDec EqDecInstances