proposition: Lemma sem_productive : forall r s, sem r s -> productive r -> s <> nil.
proof: Proof. Proof using. introv S. induction S; introv P; simpl in P; auto_false*. intros E. destruct (app_eq_nil_inv E). subst. destruct* P. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat TLC.LibNat