include "Universes.ma".

(*
ninductive Char: Type[0] ≝
  a: Char
| b: Char
| c: Char
| d: Char
| e: Char
| f: Char
| g: Char
| h: Char
| i: Char
| j: Char
| k: Char
| l: Char
| m: Char
| n: Char
| o: Char
| p: Char
| q: Char
| r: Char
| s: Char
| t: Char
| u: Char
| v: Char
| w: Char
| x: Char
| y: Char
| z: Char
| A: Char
| B: Char
| C: Char
| D: Char
| E: Char
| F: Char
| G: Char
| H: Char
| I: Char
| J: Char
| K: Char
| L: Char
| M: Char
| N: Char
| O: Char
| P: Char
| Q: Char
| R: Char
| S: Char
| T: Char
| U: Char
| V: Char
| W: Char
| X: Char
| Y: Char
| Z: Char.
*)