2.1
wnds:Windows 20005.0
FchF
C1083796271547D1083797659301C1083944509575D1083945007621C1083992991811D1083993187947
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/y SameShape(x, y)";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(@y SameShape(x, y) $ @z SameShape(z, 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="@x@z(SameShape(x, z) $ @y SameShape(x, y))";b&8;g=@;}})r&14;o=fol_fst{c=1;s="";l="";d@f=1;}u{t&8;}},p{s(i{r&1;})r&5;o&6;u{t&8;}f(t{s(i{r=fol{t="";b(s=c;,s=d;)g=@;}})r&14;o=fol_fst{c=1;s="";l="";d@f=1;}u{t&8;}},p{s(i{r&1;})r&5;o&6;u{t&8;}f(t{s(i{r=fol{t="SameShape(a, b)";b(s=a;,s=b;)g=@;}})r&14;o=fol_fst{c=1;s="";l="";d@f=1;}u{t&8;}},t{s(i{r=fol{t="SameShape(a, b) $ @y SameShape(a, y)";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="@y SameShape(a, y)";b&8;g=@;}})r{u="u\u2192 Elim";s=fol;}o=fol_fst{c=1;s="";l="";d@f=1;}u{t(p{si&48;ss=3.1.0;},p{si&55;ss=3.1.1;})}},t{s(i{r=fol{t="@y SameShape(a, y) $ @z SameShape(z, a)";b&8;g=@;}})r&57;o=fol_fst{c=1;s="";l="";d@f=1;}u{t(p{si&19;ss=1;})}},t{s(i{r=fol{t="@z SameShape(z, a)";b&8;g=@;}})r&66;o=fol_fst{c=1;s="";l="";d@f=1;}u{t(p{si&64;ss=3.1.2;},p{si&74;ss=3.1.3;})}},t{s(i{r=fol{t="SameShape(c, a)";b&8;g=@;}})r&57;o=fol_fst{c=1;s="";l="";d@f=1;}u{t(p{si&82;ss=3.1.4;})}},t{s(i{r=fol{t="SameShape(c, a) $ @y SameShape(c, y)";b&8;g=@;}})r&57;o=fol_fst{c=1;s="";l="";d@f=1;}u{t(p{si&25;ss=2;})}},t{s(i{r=fol{t="@y SameShape(c, y)";b&8;g=@;}})r&66;o=fol_fst{c=1;s="";l="";d@f=1;}u{t(p{si&91;ss=3.1.5;},p{si&99;ss=3.1.6;})}},t{s(i{r=fol{t="SameShape(c, d)";b&8;g=@;}})r&57;o=fol_fst{c=1;s="";l="";d@f=1;}u{t(p{si&107;ss=3.1.7;})}})},t{s(i{r=fol{t="SameShape(c, d)";b&8;g=@;}})r{u="u\u2203 Elim";s=fol;}o=fol_fst{c=1;s="";l="";d@f=1;}u{t(p{si&12;ss=0;},p{si&43;ss=3.1.;})}})},t{s(i{r=fol{t="@x@y SameShape(x, y)";b&8;g=@;}})r{u="u\u2200 Intro";s=fol;}o=fol_fst{c=1;s="";l="";d@f=1;}u{t(p{si&31;ss=3.;})}})}g{g&8;}a=true;}}c=166393;