proposition: Lemma poly_f_equal@{i j} : forall (A : Type@{i}) (B : Type@{j}) (f : A -> B) (x y : A), x = y -> f x = f y.
proof: Proof. intros. destruct H. reflexivity. Defined.
imports: Equations.Prop.Loader Coq(FunctionalExtensionality) Equations.Prop.DepElim Equations.Prop.Tactics Equations.Prop.FunctionalInduction