helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/sequent_viewer.xml

   1 <?xml version="1.0"?>
   2 <b:box xmlns:m="http://www.w3.org/1998/Math/MathML" xmlns:b="http://helm.cs.unibo.it/2003/BoxML" xmlns:helm="http://www.cs.unibo.it/helm" xmlns:xlink="http://www.w3.org/1999/xlink"><b:h><b:space width="0.5em"/><b:v><b:space width="0.5em"/><b:v><b:h helm:xref="h0"><b:obj><m:mi>p</m:mi></b:obj><b:text>:</b:text><b:obj><m:mi helm:xref="i1" xlink:href="cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)">nat</m:mi></b:obj></b:h><b:h helm:xref="h1"><b:obj><m:mi>n</m:mi></b:obj><b:text>:</b:text><b:obj><m:mi helm:xref="i2" xlink:href="cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)">nat</m:mi></b:obj></b:h><b:h helm:xref="h2"><b:obj><m:mi>m</m:mi></b:obj><b:text>:</b:text><b:obj><m:mi helm:xref="i3" xlink:href="cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)">nat</m:mi></b:obj></b:h><b:h helm:xref="h3"><b:obj><m:mi>H</m:mi></b:obj><b:text>:</b:text><b:hv helm:xref="i4"><b:hv helm:xref="i6"><b:obj><m:mi helm:xref="i8">p</m:mi></b:obj><b:obj><m:mrow><m:mo helm:xref="i7" xlink:href="cic:/Coq/Init/Peano/plus.con">+</m:mo><m:mi helm:xref="i9">n</m:mi></m:mrow></b:obj></b:hv><b:h><b:obj><m:mo helm:xref="i5" xlink:href="cic:/Coq/Init/Peano/le.ind#xpointer(1/1)">&#x2264;</m:mo></b:obj><b:hv helm:xref="i10"><b:obj><m:mi helm:xref="i12">p</m:mi></b:obj><b:obj><m:mrow><m:mo helm:xref="i11" xlink:href="cic:/Coq/Init/Peano/plus.con">+</m:mo><m:mi helm:xref="i13">m</m:mi></m:mrow></b:obj></b:hv></b:h></b:hv></b:h></b:v><b:ink width="4cm" height="2px"/><b:space width="0.5em"/><b:obj><m:mi helm:xref="i14" xlink:href="cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)">nat</m:mi></b:obj></b:v></b:h></b:box>