1 2 3 4 5 6 7 8
theory scratch imports HoTT begin schematic_goal "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> ?x : A \<times> B" by simple end