add a reference
Add a new syntax for testing purposes: three new types in TS format:

    [ : t Type ]
    [ : o : t ]
    [ : t == t' ]
    [ : o == o' : t ]

, which can be used in lemmas, see witnessed-judgments.ts .  But better than

  Lemma a2 [ : xf : @[Pi';_][T,@[U']] ] := _ .

would be something like

  Lemma a2 @[Pi';_][T,@[U']]
     := xf
     := _ .

, where first we give the o-expression and then the witness.