proposition: Lemma fun_beta_aeq_l f u : ~Fun f =>b u.
proof: Proof. intro r; inversion r; subst. simpl_aeq; subst. inversion H1; subst. inversion H. Qed.
imports: Coq(Wf_nat Basics Morphisms) CoLoR(RelUtil LogicUtil VecUtil VecOrd SN NatUtil)