2 <start_musing id="X;h9@Xgt=sT|HF7owBaa+h,c[DbU5-b0"><gTopLevelStatus>
3 <CurrentGoal>2</CurrentGoal>
4 <ConstantType id="1" name="dummy" params="">
6 <decl binder="x" id="i164" type="Type">
7 <CONST id="i262" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R.con"/>
10 <APPLY id="i166" sort="Type">
11 <MUTIND id="i168" noType="0" uri="cic:/Coq/Init/Logic_Type/eqT.ind"/>
12 <CONST id="i176" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R.con"/>
13 <REL binder="x" id="i178" idref="i164" sort="Type" value="1"/>
14 <APPLY id="i180" sort="Type">
15 <CONST id="i182" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rdiv.con"/>
16 <APPLY id="i188" sort="Type">
17 <CONST id="i190" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rminus.con"/>
18 <APPLY id="i196" sort="Type">
19 <CONST id="i198" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rminus.con"/>
20 <APPLY id="i204" sort="Type">
21 <CONST id="i206" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rmult.con"/>
22 <APPLY id="i212" sort="Type">
23 <CONST id="i214" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rplus.con"/>
24 <REL binder="x" id="i220" idref="i164" sort="Type" value="1"/>
25 <CONST id="i222" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R1.con"/>
27 <APPLY id="i224" sort="Type">
28 <CONST id="i226" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rplus.con"/>
29 <REL binder="x" id="i232" idref="i164" sort="Type" value="1"/>
30 <CONST id="i234" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R1.con"/>
33 <CONST id="i236" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R1.con"/>
35 <APPLY id="i238" sort="Type">
36 <CONST id="i240" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rmult.con"/>
37 <REL binder="x" id="i246" idref="i164" sort="Type" value="1"/>
38 <REL binder="x" id="i248" idref="i164" sort="Type" value="1"/>
41 <APPLY id="i250" sort="Type">
42 <CONST id="i252" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rplus.con"/>
43 <CONST id="i258" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R1.con"/>
44 <CONST id="i260" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R1.con"/>
51 <CurrentProof id="1" of="cic:/dummy.con">
52 <Conjecture id="c0" no="2">
53 <Decl id="h0" name="x">
54 <CONST id="i0" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R.con"/>
57 <APPLY id="i2" sort="Type">
58 <MUTIND id="i4" noType="0" uri="cic:/Coq/Init/Logic_Type/eqT.ind"/>
59 <CONST id="i12" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R.con"/>
60 <REL binder="x" id="i14" idref="h0" sort="Type" value="1"/>
61 <APPLY id="i16" sort="Type">
62 <CONST id="i18" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rdiv.con"/>
63 <APPLY id="i24" sort="Type">
64 <CONST id="i26" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rminus.con"/>
65 <APPLY id="i32" sort="Type">
66 <CONST id="i34" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rminus.con"/>
67 <APPLY id="i40" sort="Type">
68 <CONST id="i42" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rmult.con"/>
69 <APPLY id="i48" sort="Type">
70 <CONST id="i50" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rplus.con"/>
71 <REL binder="x" id="i56" idref="h0" sort="Type" value="1"/>
72 <CONST id="i58" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R1.con"/>
74 <APPLY id="i60" sort="Type">
75 <CONST id="i62" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rplus.con"/>
76 <REL binder="x" id="i68" idref="h0" sort="Type" value="1"/>
77 <CONST id="i70" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R1.con"/>
80 <CONST id="i72" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R1.con"/>
82 <APPLY id="i74" sort="Type">
83 <CONST id="i76" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rmult.con"/>
84 <REL binder="x" id="i82" idref="h0" sort="Type" value="1"/>
85 <REL binder="x" id="i84" idref="h0" sort="Type" value="1"/>
88 <APPLY id="i86" sort="Type">
89 <CONST id="i88" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rplus.con"/>
90 <CONST id="i94" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R1.con"/>
91 <CONST id="i96" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R1.con"/>
99 <decl binder="x" id="i98" type="Type">
100 <CONST id="i162" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R.con"/>
103 <META id="i130" no="2" sort="Prop">
105 <REL binder="x" id="i160" idref="i98" sort="Type" value="1"/>