proposition: Fact Forall2_impl X Y (R S : X -> Y -> Prop) : (forall x y, R x y -> S x y) -> forall l m, Forall2 R l m -> Forall2 S l m.
proof: Proof. induction 2; constructor; auto. Qed.
imports: Arith Lia List Permutation Relations Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)