proposition: Lemma symprod_lex A (gtA : relation A) : symprod gtA gtA << lex gtA Logic.eq gtA.
proof: Proof. intros t u tu. inversion tu; clear tu; subst. apply lex1. hyp. apply lex2. refl. hyp. Qed.
imports: Coq(Morphisms Basics) CoLoR(SN LogicUtil NatUtil VecUtil VecOrd ListUtil RelUtil)