2.1
wnds:Windows 20005.0
FchF
C1082418398820D1082418754208D1082418806795C1083104012647D1083104381104
newFormat
{p=proof{p{s(i{r&1;})r{u=uProof;s=proof;}o{c=1;s="";l="";d@}u{t()}f(t{s(i{r=fol{t="/x Cube(x) $ (Small(a) | Large(a))";b&8;g=@;}})r{u=uPremise;s=step;}o=fol_fst{c=1;s="";l="";d@f=1;}u{t&8;}},t{s(i{r=fol{t="@x (Large(x) $ /y(~Cube(y)))";b&8;g=@;}})r&14;o=fol_fst{c=1;s="";l="";d@f=1;}u{t&8;}},t{s(i{r=fol{t="@x Cube(x)";b&8;g=@;}})r&14;o=fol_fst{c=1;s="";l="";d@f=1;}u{t&8;}},t{s(i{r=fol{t="Cube(a)";b&8;g=@;}})r{u="u\u2200 Elim";s=fol;}o=fol_fst{c=1;s="";l="";d@f=1;}u{t(p{si&25;ss=2;})}},t{s(i{r=fol{t="/x Cube(x)";b&8;g=@;}})r{u="u\u2203 Intro";s=fol;}o=fol_fst{c=1;s="";l="";d@f=1;}u{t(p{si&31;ss=3;})}},t{s(i{r=fol{t="Small(a) | Large(a)";b&8;g=@;}})r{u="u\u2192 Elim";s=fol;}o=fol_fst{c=1;s="";l="";d@f=1;}u{t(p{si&12;ss=0;},p{si&40;ss=4;})}},p{s(i{r&1;})r&5;o&6;u{t&8;}f(t{s(i{r=fol{t="Large(a)";b&8;g=@;}})r&14;o=fol_fst{c=1;s="";l="";d@f=1;}u{t&8;}},t{s(i{r=fol{t="Large(a) $ /y(~Cube(y))";b&8;g=@;}})r&33;o=fol_fst{c=1;s="";l="";d@f=1;}u{t(p{si&19;ss=1;})}},t{s(i{r=fol{t="/y ~Cube(y)";b&8;g=@;}})r&51;o=fol_fst{c=1;s="";l="";d@f=1;}u{t(p{si&64;ss=6.0;},p{si&70;ss=6.1;})}},p{s(i{r&1;})r&5;o&6;u{t&8;}f(t{s(i{r=fol{t="~Cube(f)";b(s=f;)g=@;}})r&14;o=fol_fst{c=1;s="";l="";d@f=1;}u{t&8;}},t{s(i{r=fol{t="Cube(f)";b&8;g=@;}})r&33;o=fol_fst{c=1;s="";l="";d@f=1;}u{t(p{si&25;ss=2;})}},t{s(i{r=fol{t="^";b&8;g=@;}})r{u="u\u22A5 Intro";s=fol;}o=fol_fst{c=1;s="";l="";d@f=1;}u{t(p{si&92;ss=6.3.0;},p{si&99;ss=6.3.1;})}})},t{s(i{r=fol{t="^";b&8;g=@;}})r{u="u\u2203 Elim";s=fol;}o=fol_fst{c=1;s="";l="";d@f=1;}u{t(p{si&78;ss=6.2;},p{si&87;ss=6.3.;})}})},t{s(i{r=fol{t="~Large(a)";b&8;g=@;}})r{u="u\254 Intro";s=fol;}o=fol_fst{c=1;s="";l="";d@f=1;}u{t(p{si&59;ss=6.;})}},t{s(i{r=fol{t="Small(a)";b&8;g=@;}})r{u="uTaut Con";s=fol;}o=fol_con{c=1;s="";l="";d@f=1;}u{t(p{si&49;ss=5;},p{si&127;ss=7;})}},t{s(i{r=fol{t="/x Small(x)";b&8;g=@;}})r&42;o=fol_fst{c=1;s="";l="";d@f=1;}u{t(p{si&136;ss=8;})}})}g{g&8;}a=true;}}c=164868;