proposition: Lemma bound_var_S_iff n x : bound (S n) (var (S x)) <-> bound n (var x).
proof: Proof. split; intros H; inversion H; constructor; lia. Qed.
imports: List Relations Undecidability.L.L Undecidability.L.Util.L_facts ssreflect ssrbool ssrfun