600 400 True False Auto dialog south-east True False vertical True False 2 True True in True False True False True True 0 True False vertical True True False True False 0 0 True False 2 True False gtk-go-up False False 0 True False True False False 1 True True 0 True True False True False gtk-go-down True True 1 False False 1 True True 0 True False False True 3 1 True False True False Last: 0 True True 0 True False 4 4 end gtk-media-pause True True True False True False False 0 gtk-media-play True True True False True False False 1 gtk-media-next True True True False True False False 2 gtk-close True True True False True False False 3 True True 1 False True 2 500 480 True False Cic browser center-on-parent 500 480 True True False True False vertical True False True False _File True False True False _New True True False Open _Location ... True True False True False _Quit True True False _Edit True False True False _Copy True False False 0 True False 0 0 none True False True True False none True False gtk-new False False 0 True True False none True False gtk-go-back False False 1 True True False none True False gtk-go-forward False False 2 True True True False refresh none True False gtk-refresh False False 3 True True True False home none True False gtk-home False False 4 True False gtk-jump-to 2 False False 3 5 True False True True True ● True True 0 True True 6 False True 1 True True True True True False MathView False True True in True True False 1 True False WhelpResult 1 False True True True False none True False gtk-missing-image 2 True False WhelpEasterEgg 2 False True True 3 True False Graph 3 False True False vertical True True 3 in True True 0 True False 4 4 True False vertical True True 0 True True True True True 1 True True False True False 0 0 True False 2 True False gtk-find False False 0 True False Search True False False 1 False False 2 False True 1 4 True False SearchText 4 False True True 3 450 400 False title True dialog True False vertical True False spread False False end 0 True False vertical True False some informative message here ... False False 0 True True True in 717 True True False True True 1 False True 2 False 5 Find & Replace False mouse dialog True False 9 True False Find: 0 0 0 True False Replace with: 0 0 1 True True True True 1 0 True True 1 1 True False 5 True gtk-find True True False True False False 1 True True False True False 0 0 True False 2 True False gtk-find-and-replace False False 0 True False _Replace True False False 1 False False 2 gtk-cancel True True False True False False 3 0 2 2 False Matita True False True False vertical True False True False _File True False True False _New True True False _Open... True True False _Save True True False _Save as... True True False True False _Close True True False _Quit True True False _Edit True False True False False _Undo True True False False _Redo True True False True False Cut True True False Copy True True False Paste True True False Paste as pattern True True False Paste Unicode as TeX True True False Auto-expand TeX Macros True True True False Delete True True False True False Select _All True True False True False Find and replace... True True False True False Next ligature True True False Edit with e_xternal editor True True False _Script True False True False Execute 1 phrase True True False Retract 1 phrase True True False True False Execute all True True False Retract all True True False True False Execute until cursor True True False _View True False True False New CIC _browser True True False True False _Fullscreen True True False Natural deduction palette True True False True False Zoom in True True False Zoom out True True False Normal size True True False True False Pretty print notation True True True False Hide coercions True True True False True False Coercions Graph True True False Hints database True True False Terms grammar True True False TeX/UTF-8 table True True False _Debug True False True False True False _Help True False True False Contents True True False About True False False 0 True False True True True False 2 True False True False vertical True True True False vertical True True True True False Implication (⇒<sub>i</sub>) True True True 0 True True True True False Conjunction (∧<sub>i</sub>) True True True 1 True True True True False Disjunction left (∨<sub>i-l</sub>) True True True 2 True True True True False Disjunction right (∨<sub>i-r</sub>) True True True 3 True True True True False Negation (¬<sub>i</sub>) True True True 4 True True True True False Top (⊤<sub>i</sub>) True True True 5 True True True True False Universal (∀<sub>i</sub>) True True True 6 True True True True False Existential (∃<sub>i</sub>) True True True 7 True False Introduction rules False True 0 True True True False vertical True True True True False Implication (⇒<sub>e</sub>) True True True 0 True True True True False Conjunction left (∧<sub>e-l</sub>) True True True 1 True True True True False Conjunction right (∧<sub>e-r</sub>) True True True 2 True True True True False Disjunction (∨<sub>e</sub>) True True True 3 True True True True False Negation (¬<sub>e</sub>) True True True 4 True True True True False Bottom (⊥<sub>e</sub>) True True True 5 True True True True False Universal (∀<sub>e</sub>) True True True 6 True True True True False Existential (∃<sub>e</sub>) True True True 7 True False Elimination rules False True 1 True True True False vertical Reduction to Absurdity (RAA) True True True True True 0 Use lemma (lem) True True True True True 1 Discharge (discharge) True True True True True 2 True False Misc rules False True 2 False True 0 False True 0 400 True False vertical True False True False both True False True True False Retract all none True False gtk-goto-top False False True False True True False Retract 1 phrase none True False gtk-go-up False False True False True True False Execute until cursor none True False gtk-jump-to False False True False True True False Execute 1 phrase none True False gtk-go-down False False True False True True False Execute all none True False gtk-goto-bottom False False True True 0 True False vertical both True False True True False none True False gtk-stop False False False True 1 False False 0 True True True True True 1 True True 1 False True 250 500 True True vertical 380 True True True False True True False True True never in True True False char False True True 0 True True True True True True 0 True True 1 True False True False True True 0 True False False True False gtk-missing-image True False label14 False True False gtk-missing-image 1 True False label15 1 False True False gtk-missing-image 2 True False label16 2 False False True 1 False False 2 280 False Uri choice True center dialog True False vertical 4 True False end gtk-cancel True True True False True False False 0 True True True False True False 0 0 True False 2 True False gtk-index False False 0 True False Try _Selected True False False 1 False False 1 Try Constants True False True True False True False False 2 gtk-copy True True False True False False 3 True True True False True False 0 0 True False 2 True False gtk-ok False False 0 True False bla bla bla True False False 1 False False 4 gtk-go-forward True True True False True False False 5 False False end 0 True False vertical 3 True False some informative message here ... False False 0 400 True True True True True False True True 1 True False True True False URI: False False 0 True True True True 1 True True 2 False True 2 UriChoiceAbortButton