proposition: Lemma SN_symprod_fst : forall x, SN gt x -> SN gtA (fst x).
proof: Proof. induction 1. destruct x. simpl. apply SN_intro. intros. ded (H0 (y,b)). apply H2. apply left_sym. hyp. Qed.
imports: Coq(Morphisms List Basics Lia Wellfounded) CoLoR(LogicUtil RelUtil)