+ { out "TH" $2; [T.Inline (false, T.Con, trim $2, "")] }
+ | xlet ident restricts fs proof FS steps qed FS
+ { out "LET" $2; $7 @ [T.Inline (true, T.Con, trim $2, "")] }
+ | xlet ident restricts fs proof restricts FS
+ { out "LET" $2; [T.Inline (true, T.Con, trim $2, "")] }
+ | xlet ident restricts fs steps qed FS
+ { out "LET" $2; $5 @ [T.Inline (true, T.Con, trim $2, "")] }
+ | xlet ident restricts def restricts FS
+ { out "LET" $2; [T.Inline (true, T.Con, trim $2, "")] }
+ | xlet ident def restricts FS
+ { out "LET" $2; [T.Inline (true, T.Con, trim $2, "")] }