{- | Derives a contradiction from assumptions in the context

- A proof of a contradiction can be explicitly specified as an implicit argument
- `using`, `usingOnly`, and `hiding` with a single argument can be used instead of a proof to control the context

-}

{- | Given constructs a \Sigma-type:
- * `Given (x y z : A) B` is equivalent to `\Sigma (x y z : A) B`.
- * `Given {x y z} B` is equivalent to `\Sigma (x y z : _) B`
- * If `P : A -> B -> C -> \Type`, then `Given ((x,y,z) (a,b,c) : P) (Q x y z a b c)` is equivalent to `\Sigma (x a : A) (y b : B) (z c : C) (P x y z) (P a b c) (Q x y z a b c)`
- * If `l : Array A`, then `Given (x y : l) (P x y)` is equivalent to `\Sigma (j j' : Fin l.len) (P (l j) (l j'))`

-}
\meta Given

-- | {Exists} is a truncated version of {Given}. That is, `Exists a b c` is equivalent to `TruncP (Given a b c)`
\meta Exists \alias

{- | {Forall} works like {Given}, but returns a \Pi-type instead of a \Sigma-type.
- The last argument should be a type and will be used as the codomain.
- Other arguments work like arguments of {Given} with the exception that curly braces mean implicit arguments:
- * `Forall (x y : A) B` is equivalent to `\Pi (x y : A) -> B`
- * `Forall {x y : A} B` is equivalent to `\Pi {x y : A} -> B`
- * `Forall x y B` is equivalent to `\Pi (x : _) (y : _) -> B
- `* `Forall x (B 0) (B 1)` is equivalent to `\Pi (x : _) -> B 0 -> B 1
- `* `Forall {x y} {z} B` is equivalent to `\Pi {x y : _} {z : _} -> B`
- * If `P : A -> \Type`, then `Forall {x y : P} (Q x) (Q y)` is equivalent to `\Pi {x y : A} -> P x -> P y -> Q x -> Q y`

-}
\meta Forall \alias

-- | Returns either a tuple, a \new expression, or a single constructor of a data type depending on the expected type
\meta constructor