From Coq Require Import Int63 PArray. Open Scope array_scope. Definition t1 : array nat := [| 3; 3; 3; 3 | 3 |]. Definition t2 := [|Type|Type|].