proposition: Lemma app_free_app_no_0 : forall (t : term), app_free t <-> app_no t = 0.
proof: Proof. elim => [n | x | t1 _ t2 _ | t IHt ]; split; intros H; solve [ inversion H; (try apply IHt); subst; auto | constructor; try apply IHt; auto ]. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype) String QuickChick(QuickChick) Arith List Lia QuickChick.stlc(lambda) Wellfounded