A:Type, P:(A
Prop), n:
, X:(A^n). (
u in X: A^n. P(u)) 
Propn:. n
2 
(A^n) = A
(A^(n-1))| Theorem | Name |
| A:Type, P:(AProp), n:, X:(A^n). ( u in X: A^n. P(u)) Prop | [sfa_doc_ntuple_contains_wf] |
| cites the following: | |
| n:. n2 (A^n) = A(A^(n-1)) | [sfa_doc_ntuple_is_prod] |