Generalization problem.holbert

[{"tag":"Heading","contents":[0,"Problem demo"]},{"tag":"Rule","contents":["Inductive",[["pi-elim",[["f","x","B","a","A"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":4}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Pi"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":2}]}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_$_"},{"tag":"LocalVar","contents":4}]},{"tag":"LocalVar","contents":1}]}]},{"tag":"Ap","contents":[{"tag":"LocalVar","contents":2},{"tag":"LocalVar","contents":1}]}]}],null]],[[{"tag":"Cases","contents":["_:_",2]},[["§P","§0","§1"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]}],[["f","x","B","a","A"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_=_"},{"tag":"LocalVar","contents":6}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_$_"},{"tag":"LocalVar","contents":4}]},{"tag":"LocalVar","contents":1}]}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_=_"},{"tag":"LocalVar","contents":5}]},{"tag":"Ap","contents":[{"tag":"LocalVar","contents":2},{"tag":"LocalVar","contents":1}]}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":4}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Pi"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":2}]}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]}]],{"tag":"LocalVar","contents":7}]],{"tag":"LocalVar","contents":2}]],[{"tag":"Induction","contents":["_:_",2]},[["§P0","§0","§1"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]}],[["f","x","B","a","A"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"LocalVar","contents":7},{"tag":"LocalVar","contents":4}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Pi"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":2}]}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"LocalVar","contents":7},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":4}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Pi"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":2}]}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"LocalVar","contents":7},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_$_"},{"tag":"LocalVar","contents":4}]},{"tag":"LocalVar","contents":1}]}]},{"tag":"Ap","contents":[{"tag":"LocalVar","contents":2},{"tag":"LocalVar","contents":1}]}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"LocalVar","contents":2},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]}]]]]},{"tag":"Rule","contents":["Theorem",[["test",[["p","A","a"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":2}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Pi"},{"tag":"LocalVar","contents":1}]},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"Const","contents":"T"},{"tag":"LocalVar","contents":0}]}]}]}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":1}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_$_"},{"tag":"LocalVar","contents":2}]},{"tag":"LocalVar","contents":0}]}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"T"},{"tag":"LocalVar","contents":0}]}]}],[[null,["p","A","a"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":2}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Pi"},{"tag":"LocalVar","contents":1}]},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"Const","contents":"T"},{"tag":"LocalVar","contents":0}]}]}]}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":1}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_$_"},{"tag":"LocalVar","contents":2}]},{"tag":"LocalVar","contents":0}]}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"T"},{"tag":"LocalVar","contents":0}]}]},null],5]]],[]]}]