theorem exists_in_reality
theorem exists_in_reality
(i : FoolUnderstandsTheWords)
(ii : WhateverIsUnderstoodExistsInTheUnderstanding)
(iii_bridge : ExistsInUnderstandingBridge)
⋯4 more premises
: ExistsInReality