1
Inductive sig2 (A : Type) (P Q : A -> Prop) : Type :=
2
exist2 : forall x : A, P x -> Q x -> sig2 P Q
4
For sig2: Argument A is implicit
5
For exist2: Argument A is implicit
6
For sig2: Argument scopes are [type_scope type_scope type_scope]
7
For exist2: Argument scopes are [type_scope _ _ _ _ _]
10
fun b : bool => if b then b else b