証明のデータ型としての命題