proposition: Lemma clos_refl_trans_flip {X : Type} {R : X -> X -> Prop} {x y} : clos_refl_trans _ R x y -> clos_refl_trans _ (fun y x => R x y) y x.
proof: Proof. by elim; eauto using clos_refl_trans. Qed.
imports: Undecidability.LambdaCalculus.Lambda PeanoNat Lia List Relations ssreflect