theorem Hex.RCF.decide_sound (s : Sentence) (h : decide s = some true) : s.toProp

Every true compiled verdict proves the reflected sentence.