Nuprl - Pf fvar wf

(2steps) PrintForm Definitions formula Sections ClassicalProps(jlc) Doc

At: fvar wf

x:Var. x Formula

By: Unfold `fvar` 0

Generated subgoal:

1 1. x: Var
inl(x) Formula

About:

(2steps) PrintForm Definitions formula Sections ClassicalProps(jlc) Doc