-<prova>
- <ciao/>
-</prova>
+<?xml version="1.0" encoding="iso-8859-1"?>
+<?cocoon-format type="text/xhtml"?>
+<m:math xmlns:helm="http://www.cs.unibo.it/helm" xmlns:m="http://www.w3.org/1998/Math/MathML">
+ <m:mtable helm:xref="i0" columnalign="left" equalrows="false" align="baseline 1">
+ <m:mtr>
+ <m:mtd>
+ <m:mrow>
+ <m:mtext>DEFINITION and_ind() OF TYPE</m:mtext>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ <m:mtr>
+ <m:mtd>
+ <m:mrow>
+ <m:mphantom>
+ <m:mtext>__</m:mtext>
+ </m:mphantom>
+ <m:semantics xmlns:xlink="http://www.w3.org/1999/xlink">
+ <m:mrow helm:xref="i22">
+ <m:mtable columnalign="left" equalrows="false" align="baseline 1">
+ <m:mtr>
+ <m:mtd>
+ <m:mrow>
+ <m:mo stretchy="false">(</m:mo>
+ <m:mrow helm:xref="i23">
+ <m:mtable columnalign="left" equalrows="false" align="baseline 1">
+ <m:mtr>
+ <m:mtd>
+ <m:mo color="Blue">Π</m:mo>
+ <m:mi>A</m:mi>
+ <m:mo>:</m:mo>
+ <m:mrow helm:xref="i24">
+ <m:mo>Prop</m:mo>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ <m:mtr>
+ <m:mtd>
+ <m:mrow>
+ <m:mo>.</m:mo>
+ <m:mrow helm:xref="i25">
+ <m:mtable columnalign="left" equalrows="false" align="baseline 1">
+ <m:mtr>
+ <m:mtd>
+ <m:mo color="Blue">Π</m:mo>
+ <m:mi>B</m:mi>
+ <m:mo>:</m:mo>
+ <m:mrow helm:xref="i26">
+ <m:mo>Prop</m:mo>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ <m:mtr>
+ <m:mtd>
+ <m:mrow>
+ <m:mo>.</m:mo>
+ <m:mrow helm:xref="i27">
+ <m:mtable columnalign="left" equalrows="false" align="baseline 1">
+ <m:mtr>
+ <m:mtd>
+ <m:mo color="Blue">Π</m:mo>
+ <m:mi>P</m:mi>
+ <m:mo>:</m:mo>
+ <m:mrow helm:xref="i28">
+ <m:mo>Prop</m:mo>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ <m:mtr>
+ <m:mtd>
+ <m:mrow>
+ <m:mo>.</m:mo>
+ <m:mrow helm:xref="i29">
+ <m:mtable columnalign="left" equalrows="false" align="baseline 1">
+ <m:mtr>
+ <m:mtd>
+ <m:mo color="Blue">Π</m:mo>
+ <m:mi>f</m:mi>
+ <m:mo>:</m:mo>
+ <m:mrow helm:xref="i30">
+ <m:mo stretchy="false">(</m:mo>
+ <m:mi helm:xref="i31">A</m:mi>
+ <m:mo color="Blue">→</m:mo>
+ <m:mrow helm:xref="i32">
+ <m:mo stretchy="false">(</m:mo>
+ <m:mi helm:xref="i33">B</m:mi>
+ <m:mo color="Blue">→</m:mo>
+ <m:mi helm:xref="i34">P</m:mi>
+ <m:mo stretchy="false">)</m:mo>
+ </m:mrow>
+ <m:mo stretchy="false">)</m:mo>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ <m:mtr>
+ <m:mtd>
+ <m:mrow>
+ <m:mo>.</m:mo>
+ <m:mrow helm:xref="i35">
+ <m:mo color="Blue">Π</m:mo>
+ <m:mi>a</m:mi>
+ <m:mo>:</m:mo>
+ <m:mrow helm:xref="i36">
+ <m:mo stretchy="false">(</m:mo>
+ <m:mi xlink:href="cic:/coq/INIT/Logic/Conjunction/and.ind" helm:xref="i37">and</m:mi>
+ <m:mphantom>
+ <m:mtext>_</m:mtext>
+ </m:mphantom>
+ <m:mi helm:xref="i38">A</m:mi>
+ <m:mphantom>
+ <m:mtext>_</m:mtext>
+ </m:mphantom>
+ <m:mi helm:xref="i39">B</m:mi>
+ <m:mo stretchy="false">)</m:mo>
+ </m:mrow>
+ <m:mo>.</m:mo>
+ <m:mi helm:xref="i40">P</m:mi>
+ </m:mrow>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ </m:mtable>
+ </m:mrow>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ </m:mtable>
+ </m:mrow>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ </m:mtable>
+ </m:mrow>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ </m:mtable>
+ </m:mrow>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ <m:mtr>
+ <m:mtd>
+ <m:mrow>
+ <m:mo color="#b03060">:></m:mo>
+ <m:mrow helm:xref="i41">
+ <m:mo>Prop</m:mo>
+ </m:mrow>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ <m:mtr>
+ <m:mtd>
+ <m:mrow>
+ <m:mo stretchy="false">)</m:mo>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ </m:mtable>
+ </m:mrow>
+ <m:annotation-xml encoding="MathML">
+ <m:apply helm:xref="i22">
+ <m:csymbol>cast</m:csymbol>
+ <m:apply helm:xref="i23">
+ <m:csymbol>prod</m:csymbol>
+ <m:bvar>
+ <m:ci>A</m:ci>
+ <m:type>
+ <m:apply helm:xref="i24">
+ <m:csymbol>Prop</m:csymbol>
+ </m:apply>
+ </m:type>
+ </m:bvar>
+ <m:apply helm:xref="i25">
+ <m:csymbol>prod</m:csymbol>
+ <m:bvar>
+ <m:ci>B</m:ci>
+ <m:type>
+ <m:apply helm:xref="i26">
+ <m:csymbol>Prop</m:csymbol>
+ </m:apply>
+ </m:type>
+ </m:bvar>
+ <m:apply helm:xref="i27">
+ <m:csymbol>prod</m:csymbol>
+ <m:bvar>
+ <m:ci>P</m:ci>
+ <m:type>
+ <m:apply helm:xref="i28">
+ <m:csymbol>Prop</m:csymbol>
+ </m:apply>
+ </m:type>
+ </m:bvar>
+ <m:apply helm:xref="i29">
+ <m:csymbol>prod</m:csymbol>
+ <m:bvar>
+ <m:ci>f</m:ci>
+ <m:type>
+ <m:apply helm:xref="i30">
+ <m:csymbol>arrow</m:csymbol>
+ <m:ci helm:xref="i31">A</m:ci>
+ <m:apply helm:xref="i32">
+ <m:csymbol>arrow</m:csymbol>
+ <m:ci helm:xref="i33">B</m:ci>
+ <m:ci helm:xref="i34">P</m:ci>
+ </m:apply>
+ </m:apply>
+ </m:type>
+ </m:bvar>
+ <m:apply helm:xref="i35">
+ <m:csymbol>prod</m:csymbol>
+ <m:bvar>
+ <m:ci>a</m:ci>
+ <m:type>
+ <m:apply helm:xref="i36">
+ <m:csymbol>app</m:csymbol>
+ <m:ci definitionURL="cic:/coq/INIT/Logic/Conjunction/and.ind" helm:xref="i37">and</m:ci>
+ <m:ci helm:xref="i38">A</m:ci>
+ <m:ci helm:xref="i39">B</m:ci>
+ </m:apply>
+ </m:type>
+ </m:bvar>
+ <m:ci helm:xref="i40">P</m:ci>
+ </m:apply>
+ </m:apply>
+ </m:apply>
+ </m:apply>
+ </m:apply>
+ <m:apply helm:xref="i41">
+ <m:csymbol>Prop</m:csymbol>
+ </m:apply>
+ </m:apply>
+ </m:annotation-xml>
+ </m:semantics>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ <m:mtr>
+ <m:mtd>
+ <m:mrow>
+ <m:mtext>AS</m:mtext>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ <m:mtr>
+ <m:mtd>
+ <m:mrow>
+ <m:mphantom>
+ <m:mtext>__</m:mtext>
+ </m:mphantom>
+ <m:semantics xmlns:xlink="http://www.w3.org/1999/xlink">
+ <m:mrow helm:xref="i1">
+ <m:mtable columnalign="left" equalrows="false" align="baseline 1">
+ <m:mtr>
+ <m:mtd>
+ <m:mo color="Red">λ</m:mo>
+ <m:mi>A</m:mi>
+ <m:mo>:</m:mo>
+ <m:mrow helm:xref="i2">
+ <m:mo>Prop</m:mo>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ <m:mtr>
+ <m:mtd>
+ <m:mrow>
+ <m:mo>.</m:mo>
+ <m:mrow helm:xref="i3">
+ <m:mtable columnalign="left" equalrows="false" align="baseline 1">
+ <m:mtr>
+ <m:mtd>
+ <m:mo color="Red">λ</m:mo>
+ <m:mi>B</m:mi>
+ <m:mo>:</m:mo>
+ <m:mrow helm:xref="i4">
+ <m:mo>Prop</m:mo>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ <m:mtr>
+ <m:mtd>
+ <m:mrow>
+ <m:mo>.</m:mo>
+ <m:mrow helm:xref="i5">
+ <m:mtable columnalign="left" equalrows="false" align="baseline 1">
+ <m:mtr>
+ <m:mtd>
+ <m:mo color="Red">λ</m:mo>
+ <m:mi>P</m:mi>
+ <m:mo>:</m:mo>
+ <m:mrow helm:xref="i6">
+ <m:mo>Prop</m:mo>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ <m:mtr>
+ <m:mtd>
+ <m:mrow>
+ <m:mo>.</m:mo>
+ <m:mrow helm:xref="i7">
+ <m:mtable columnalign="left" equalrows="false" align="baseline 1">
+ <m:mtr>
+ <m:mtd>
+ <m:mo color="Red">λ</m:mo>
+ <m:mi>f</m:mi>
+ <m:mo>:</m:mo>
+ <m:mrow helm:xref="i8">
+ <m:mo stretchy="false">(</m:mo>
+ <m:mi helm:xref="i9">A</m:mi>
+ <m:mo color="Blue">→</m:mo>
+ <m:mrow helm:xref="i10">
+ <m:mo stretchy="false">(</m:mo>
+ <m:mi helm:xref="i11">B</m:mi>
+ <m:mo color="Blue">→</m:mo>
+ <m:mi helm:xref="i12">P</m:mi>
+ <m:mo stretchy="false">)</m:mo>
+ </m:mrow>
+ <m:mo stretchy="false">)</m:mo>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ <m:mtr>
+ <m:mtd>
+ <m:mrow>
+ <m:mo>.</m:mo>
+ <m:mrow helm:xref="i13">
+ <m:mtable columnalign="left" equalrows="false" align="baseline 1">
+ <m:mtr>
+ <m:mtd>
+ <m:mo color="Red">λ</m:mo>
+ <m:mi>a</m:mi>
+ <m:mo>:</m:mo>
+ <m:mrow helm:xref="i14">
+ <m:mo stretchy="false">(</m:mo>
+ <m:mi xlink:href="cic:/coq/INIT/Logic/Conjunction/and.ind" helm:xref="i15">and</m:mi>
+ <m:mphantom>
+ <m:mtext>_</m:mtext>
+ </m:mphantom>
+ <m:mi helm:xref="i16">A</m:mi>
+ <m:mphantom>
+ <m:mtext>_</m:mtext>
+ </m:mphantom>
+ <m:mi helm:xref="i17">B</m:mi>
+ <m:mo stretchy="false">)</m:mo>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ <m:mtr>
+ <m:mtd>
+ <m:mrow>
+ <m:mo>.</m:mo>
+ <m:mrow helm:xref="i18">
+ <m:mo><</m:mo>
+ <m:mi helm:xref="i19">P</m:mi>
+ <m:mo>></m:mo>
+ <m:mo>CASES</m:mo>
+ <m:mphantom>
+ <m:mtext>_</m:mtext>
+ </m:mphantom>
+ <m:mi helm:xref="i20">a</m:mi>
+ <m:mphantom>
+ <m:mtext>_</m:mtext>
+ </m:mphantom>
+ <m:mo>OF</m:mo>
+ <m:mrow>
+ <m:mo stretchy="false">(</m:mo>
+ <m:mi>conj</m:mi>
+ <m:mphantom>
+ <m:mtext>_</m:mtext>
+ </m:mphantom>
+ <m:mi>$1</m:mi>
+ <m:mphantom>
+ <m:mtext>_</m:mtext>
+ </m:mphantom>
+ <m:mi>$2</m:mi>
+ <m:mo stretchy="false">)</m:mo>
+ </m:mrow>
+ <m:mo color="Green">⇒</m:mo>
+ <m:mrow>
+ <m:mo stretchy="false">(</m:mo>
+ <m:mi helm:xref="i21">f</m:mi>
+ <m:mphantom>
+ <m:mtext>_</m:mtext>
+ </m:mphantom>
+ <m:mi>$1</m:mi>
+ <m:mphantom>
+ <m:mtext>_</m:mtext>
+ </m:mphantom>
+ <m:mi>$2</m:mi>
+ <m:mo stretchy="false">)</m:mo>
+ </m:mrow>
+ <m:mphantom>
+ <m:mtext>_</m:mtext>
+ </m:mphantom>
+ <m:mo>END</m:mo>
+ </m:mrow>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ </m:mtable>
+ </m:mrow>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ </m:mtable>
+ </m:mrow>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ </m:mtable>
+ </m:mrow>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ </m:mtable>
+ </m:mrow>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ </m:mtable>
+ </m:mrow>
+ <m:annotation-xml encoding="MathML">
+ <m:lambda helm:xref="i1">
+ <m:bvar>
+ <m:ci>A</m:ci>
+ <m:type>
+ <m:apply helm:xref="i2">
+ <m:csymbol>Prop</m:csymbol>
+ </m:apply>
+ </m:type>
+ </m:bvar>
+ <m:lambda helm:xref="i3">
+ <m:bvar>
+ <m:ci>B</m:ci>
+ <m:type>
+ <m:apply helm:xref="i4">
+ <m:csymbol>Prop</m:csymbol>
+ </m:apply>
+ </m:type>
+ </m:bvar>
+ <m:lambda helm:xref="i5">
+ <m:bvar>
+ <m:ci>P</m:ci>
+ <m:type>
+ <m:apply helm:xref="i6">
+ <m:csymbol>Prop</m:csymbol>
+ </m:apply>
+ </m:type>
+ </m:bvar>
+ <m:lambda helm:xref="i7">
+ <m:bvar>
+ <m:ci>f</m:ci>
+ <m:type>
+ <m:apply helm:xref="i8">
+ <m:csymbol>arrow</m:csymbol>
+ <m:ci helm:xref="i9">A</m:ci>
+ <m:apply helm:xref="i10">
+ <m:csymbol>arrow</m:csymbol>
+ <m:ci helm:xref="i11">B</m:ci>
+ <m:ci helm:xref="i12">P</m:ci>
+ </m:apply>
+ </m:apply>
+ </m:type>
+ </m:bvar>
+ <m:lambda helm:xref="i13">
+ <m:bvar>
+ <m:ci>a</m:ci>
+ <m:type>
+ <m:apply helm:xref="i14">
+ <m:csymbol>app</m:csymbol>
+ <m:ci definitionURL="cic:/coq/INIT/Logic/Conjunction/and.ind" helm:xref="i15">and</m:ci>
+ <m:ci helm:xref="i16">A</m:ci>
+ <m:ci helm:xref="i17">B</m:ci>
+ </m:apply>
+ </m:type>
+ </m:bvar>
+ <m:apply helm:xref="i18">
+ <m:csymbol>mutcase</m:csymbol>
+ <m:ci helm:xref="i19">P</m:ci>
+ <m:ci helm:xref="i20">a</m:ci>
+ <m:apply>
+ <m:csymbol>app</m:csymbol>
+ <m:ci>conj</m:ci>
+ <m:ci>$1</m:ci>
+ <m:ci>$2</m:ci>
+ </m:apply>
+ <m:apply>
+ <m:csymbol>app</m:csymbol>
+ <m:ci helm:xref="i21">f</m:ci>
+ <m:ci>$1</m:ci>
+ <m:ci>$2</m:ci>
+ </m:apply>
+ </m:apply>
+ </m:lambda>
+ </m:lambda>
+ </m:lambda>
+ </m:lambda>
+ </m:lambda>
+ </m:annotation-xml>
+ </m:semantics>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ </m:mtable>
+</m:math>