proposition: Lemma algebraic_dec: forall M, {algebraic M} + {~algebraic M}.
proof: Proof. intro M. apply well_founded_induction with (R := subterm) (P := fun M => {algebraic M} + {~algebraic M}). apply subterm_wf. clear M; intros M IH. destruct (term_case M) as [[[Mvar | Mfun] | Mabs] | Mapp]. left; apply AlgVar; trivial. destruct (baseType_dec (type M)). left; apply AlgFunApp; term_inv M. assert (forall T, isBaseType T -> isArrowType T -> False). destruct T; trivial. right; intro Marg; inversion Marg; term_inv M. apply H with (f_type f); trivial. destruct (IH (absBody Mabs) (absBody_subterm M Mabs)). left; apply AlgAbs with Mabs; trivial. right; intro Malg; inversion Malg; term_inv M. destruct (isFunApp_dec M) as [Mfapp | Mnfapp]. destruct (baseType_dec (type M)). destruct (list_dec_all (fun M => algebraic M) (appArgs M)). intros; apply IH. apply arg_subterm; trivial. left; apply AlgFunApp; trivial. right; intro Marg; inversion Marg; try solve [term_inv M]. destruct e as [l [lM lalg]]. absurd (algebraic l); trivial. apply H1; trivial. right; intro Marg; inversion Marg; term_inv M. destruct B; try_solve. destruct (list_dec_all (fun M => algebraic M) (appUnits M)). intros; apply IH. apply appUnit_subterm; trivial. left; apply AlgApp; trivial. right; intro Marg; inversion Marg; term_inv M. destruct e as [l [lM lalg]]. absurd (algebraic l); trivial. apply H1; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsEta LogicUtil) Coq(Morphisms)