>There is a bit of a conflict between proof length and amount of DV conditions.
>So far, I've been inclined to prefer fewer DV conditions at the cost of longer proofs, because theorems can be used more easily later, as in the example above. >What version do people usually prefer? My vote, in general, is for fewer DV conditions, even at the cost of a longer proof. I also prefer using nf* over cbv*, as it makes the intent clearer. -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion visit https://groups.google.com/d/msgid/metamath/c785d05d-99a9-4dfe-83e6-1e4d05a6a061n%40googlegroups.com.
