proposition: Lemma eq_pair_dec : forall (A B : Type), (forall x y : A, {x = y} + {x <> y}) -> (forall x y : B, {x = y} + {x <> y}) -> (forall x y : A * B, {x = y} + {x <> y}).
proof: Proof. decide equality. Qed.
imports: Coq.Lists.List Coq.Logic.Eqdep_dec Lia