ded5.ivy

#lang ivy1.7

include deduction

theorem [nonce] {
    type t
    individual x : t
    relation p
    property [triv] p
    property p
}
proof
    apply triv

theorem [andA2] {
    type t
    function p(X:t) : bool
    function q : bool
    property forall X. p(X) & q
    property (forall X. p(X)) & q
}
proof
    apply introAnd;
    apply introA;
    apply elimAndL with q = q;
    apply elimA with X=x;
    apply nonce;
    apply elimAndR with p = p(x);
    apply elimA with X=x


theorem [thing] {
   type u