proposition: Theorem rel_dec_sym : Symmetric eqt -> forall x y, x ?[ eqt ] y = y ?[ eqt ] x.
proof: Proof. intros. remember (x ?[ eqt ] y); remember (y ?[ eqt ] x); intuition. destruct b; destruct b0; auto. { symmetry in Heqb; symmetry in Heqb0. eapply (@rel_dec_correct _ _ _ rc) in Heqb. symmetry in Heqb. eapply (@rel_dec_correct _ _ _ rc) in Heqb. congruence. } { symmetry in Heqb; symmetry in Heqb0. eapply (@rel_dec_correct _ _ _ rc) in Heqb0. symmetry in Heqb0. eapply (@rel_dec_correct _ _ _ rc) in Heqb0. congruence. } Qed.
imports: Coq.Bool.Bool Coq.Classes.RelationClasses