fact: Definition substitution (x y : term) : option (term * term) := match x, y with | Var n, Var m => if Pos.eq_dec n m then None else Some (x, y) | Var _, _ => Some (x, y) | _ , Var _ => Some (y, x) | _, _ => None end.
imports: Coq.NArith.NArith Coq.FSets.FMaps Coq.micromega.Lia Category.Lib Category.Lib.FMapExt