proposition: Lemma evalDet_left_total : forall (A : Set)(c : Comp A) s, well_formed_comp c -> exists ans, evalDet c s ans.
proof: Proof. intuition. edestruct (evalDet_dec). eauto. destruct H0. econstructor. eauto. econstructor. eauto. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia