proposition: Lemma boundE k s : bound k s -> match s with | var n => k > n | app s t => bound k s /\ bound k t | lam s => bound (S k) s end.
proof: Proof. by case. Qed.
imports: List Relations Undecidability.L.L Undecidability.L.Util.L_facts ssreflect ssrbool ssrfun