Theorem componentValueWFDecidable : forall (v : componentValueT), {componentValueWF v}+{~componentValueWF v}.
