proposition: Lemma SN_symprod_inv : forall x y, SN gt (x,y) -> SN gtA x /\ SN gtB y.
proof: Proof. intros. split. eapply SN_symprod_invl. apply H. eapply SN_symprod_invr. apply H. Qed.
imports: Coq(Morphisms List Basics Lia Wellfounded) CoLoR(LogicUtil RelUtil)