| C.AConstant (_, _, s, None, t, [], attrs) ->
[T.Statement (`Axiom, Some s, t, None, "")]
| C.AInductiveDefinition (_, types, [], lpsno, attrs) ->
| C.AConstant (_, _, s, None, t, [], attrs) ->
[T.Statement (`Axiom, Some s, t, None, "")]
| C.AInductiveDefinition (_, types, [], lpsno, attrs) ->