fact: Fixpoint closed_aux acc t := match t with | Cst _ => true | Lam s t' => closed_aux (cons s acc) t' | Var n => if List.in_dec string_dec n acc then true else false | App t₁ t₂ => closed_aux acc t₁ && closed_aux acc t₂ end.
imports: Bool String Coq.Classes.RelationClasses