proposition: Theorem evalDet_steps_trans : forall (A : Set)(x y : comp_state A), evalDet_steps x y -> forall z, evalDet_steps y z -> evalDet_steps x z.
proof: Proof. induction 1; intuition; subst. econstructor. trivial. eapply IHevalDet_steps. trivial. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia