ctaipycmaci lujvo

x1 is a type theory.