Compact premise and goal composer with visible RHS nesting.
Just the shared proposition list. No values here.
Set each side to blank or NOT. Use Nested RHS to build stepped formulas like p implies (q implies r).