- if (conclude.Con.conclude_method = "RewriteLR" && is_top_down)
- || (conclude.Con.conclude_method = "RewriteRL" && not is_top_down) then
- B.V([], [justif1 ; B.H([],[B.b_kw "we proved (" ; term1 ; B.b_kw "=" ; term2; B.b_kw ") (equality)."]); B.b_kw "by _"])
- else
- B.V([], [justif1 ; B.H([],[B.b_kw "we proved (" ; term2 ; B.b_kw "=" ; term1; B.b_kw ") (equality)."]); B.b_kw "by _"])
-(*CSC: bad idea
- B.V([], [B.H([],[B.b_kw "obtain fooo " ; term2 ; B.b_kw "=" ; term1; B.b_kw "by" ; B.b_kw "proof" ; B.Text([],"."); justif1])]) *)