rigid form 是 dependent type 中即使是 open term 也必須先進行計算而被迫在實作中出現的一種值；由於 meta variable 而被迫出現的值則叫做 flex form