ndefinition hint_declaration_CProp0 ≝ λA:CProp[0].λa,b:A.Prop.
ndefinition hint_declaration_CProp1 ≝ λA:CProp[1].λa,b:A.Prop.
ndefinition hint_declaration_CProp0 ≝ λA:CProp[0].λa,b:A.Prop.
ndefinition hint_declaration_CProp1 ≝ λA:CProp[1].λa,b:A.Prop.