proposition: Lemma var_in_cand : forall (n : nat) (X : term -> Prop), is_cand X -> X (Ref n).
proof: Proof. intros. apply (clos_exp X); auto with coc core arith datatypes. unfold neutral in |- *; intros; discriminate. intros. inversion H0. Qed.
imports: Termes Conv Types Class