proposition: Lemma SN_symprod_snd : forall x, SN gt x -> SN gtB (snd x).
proof: Proof. induction 1. destruct x. simpl. apply SN_intro. intros. ded (H0 (a,y)). apply H2. apply right_sym. hyp. Qed.
imports: Coq(Morphisms List Basics Lia Wellfounded) CoLoR(LogicUtil RelUtil)