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.