Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- Inductive pi : Type :=
- | forall_pi : Type -> (Type->Type) -> pi.
- Notation "forall id : A, B" := forall_pi A (fun id => B).
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement
