proposition: Lemma evalDet_equiv_symm : forall (A : Set)(c1 c2 : Comp A), evalDet_equiv c1 c2 -> evalDet_equiv c2 c1.
proof: Proof. unfold evalDet_equiv. intuition. eapply H; trivial. eapply H; trivial. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia