interpretation "constructive ternary and" 'and3 x y z = (Conj3 x y z).
inductive And4 (A,B,C,D:CProp) : CProp ≝
| Conj4 : A → B → C → D → And4 A B C D.
interpretation "constructive ternary and" 'and3 x y z = (Conj3 x y z).
inductive And4 (A,B,C,D:CProp) : CProp ≝
| Conj4 : A → B → C → D → And4 A B C D.