proposition: Lemma clos_trans_swap s t : clos_trans step s t -> clos_trans (fun t' s' => step s' t') t s.
proof: Proof. elim; by eauto using @clos_trans with nocore. Qed.
imports: Undecidability.LambdaCalculus(Lambda Util.term_facts Util.wCBN_facts) Undecidability(L.Util.L_facts) Coq(Relations Wellfounded.Transitive_Closure List Lia) Coq(ssreflect)