quit.
#load "go".
#query top hopeb Out.
html_init.
go.
html.
nat_l "lambda n ((forall u (forall v ((plus 0 u v) => (plus u 0 v)))) => (forall m (forall p ((plus n m p) => (plus m n p)))))" 1.
imp_r.
initial 1.
html.
imp_r.
imp_l 2.
initial 1.
go.
dr plusP 1.
nat_l "lambda n g" 1.
nat_l "lambda n (plus 0 0 0)" 1.
nat_l "lambda n (forall m (plus m m m))" 1.
nat_l "lambda n (forall m (forall p ((plus n m p) => (plus m n p))))" 1.
nat_l "lambda m (forall p ((plus 0 m p) => (plus m 0 p)))" 1).
nat_l "lambda n (forall m (forall p ((plus n m p) => (plus m n p))))" 1.
nat_l "lambda w (plus w 0 w)" 1.
nat_l "lambda n (forall m (forall p ((plus n m p) => (plus m n p))))" 1.