proposition: Lemma has_var_zero_dec M : has_var_zero M \/ exists M', M = ren S M'.
proof: Proof. case: (@allfv_dec (fun n => match n with 0 => False | _ => True end) M). - move=> [|?]; tauto. - move=> H. right. exists (ren Nat.pred M). rewrite simpl_term. rewrite -[LHS]ren_id_term. apply: ext_allfv_ren_term. by apply: allfv_impl H => - [|?]. - move=> ?. by left. Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.LambdaCalculus.Util.term_facts PeanoNat Relations List Lia ssreflect