I: pbuilder: network access will be disabled during build
I: Current time: Tue May 30 23:06:53 +14 2023
I: pbuilder-time-stamp: 1685437613
I: Building the build Environment
I: extracting base tarball [/var/cache/pbuilder/bookworm-reproducible-base.tgz]
I: copying local configuration
W: --override-config is not set; not updating apt.conf Read the manpage for details.
I: mounting /proc filesystem
I: mounting /sys filesystem
I: creating /{dev,run}/shm
I: mounting /dev/pts filesystem
I: redirecting /dev/ptmx to /dev/pts/ptmx
I: policy-rc.d already exists
I: Copying source file
I: copying [coq-unicoq_1.6-8.16-2.dsc]
I: copying [./coq-unicoq_1.6-8.16.orig.tar.gz]
I: copying [./coq-unicoq_1.6-8.16-2.debian.tar.xz]
I: Extracting source
gpgv: Signature made Wed Jan 25 21:51:39 2023 +14
gpgv:                using RSA key 812EEFD8A3FBA4ACE4DF114B04C53BD7FE030551
gpgv:                issuer "jpuydt@debian.org"
gpgv: Can't check signature: No public key
dpkg-source: warning: cannot verify inline signature for ./coq-unicoq_1.6-8.16-2.dsc: no acceptable signature found
dpkg-source: info: extracting coq-unicoq in coq-unicoq-1.6-8.16
dpkg-source: info: unpacking coq-unicoq_1.6-8.16.orig.tar.gz
dpkg-source: info: unpacking coq-unicoq_1.6-8.16-2.debian.tar.xz
I: Not using root during the build.
I: Installing the build-deps
I: user script /srv/workspace/pbuilder/21008/tmp/hooks/D01_modify_environment starting
debug: Running on ff64a.
I: Changing host+domainname to test build reproducibility
I: Adding a custom variable just for the fun of it...
I: Changing /bin/sh to bash
'/bin/sh' -> '/bin/bash'
lrwxrwxrwx 1 root root 9 May 30 23:07 /bin/sh -> /bin/bash
I: Setting pbuilder2's login shell to /bin/bash
I: Setting pbuilder2's GECOS to second user,second room,second work-phone,second home-phone,second other
I: user script /srv/workspace/pbuilder/21008/tmp/hooks/D01_modify_environment finished
I: user script /srv/workspace/pbuilder/21008/tmp/hooks/D02_print_environment starting
I: set
  BASH=/bin/sh
  BASHOPTS=checkwinsize:cmdhist:complete_fullquote:extquote:force_fignore:globasciiranges:globskipdots:hostcomplete:interactive_comments:patsub_replacement:progcomp:promptvars:sourcepath
  BASH_ALIASES=()
  BASH_ARGC=()
  BASH_ARGV=()
  BASH_CMDS=()
  BASH_LINENO=([0]="12" [1]="0")
  BASH_LOADABLES_PATH=/usr/local/lib/bash:/usr/lib/bash:/opt/local/lib/bash:/usr/pkg/lib/bash:/opt/pkg/lib/bash:.
  BASH_SOURCE=([0]="/tmp/hooks/D02_print_environment" [1]="/tmp/hooks/D02_print_environment")
  BASH_VERSINFO=([0]="5" [1]="2" [2]="15" [3]="1" [4]="release" [5]="arm-unknown-linux-gnueabihf")
  BASH_VERSION='5.2.15(1)-release'
  BUILDDIR=/build
  BUILDUSERGECOS='second user,second room,second work-phone,second home-phone,second other'
  BUILDUSERNAME=pbuilder2
  BUILD_ARCH=armhf
  DEBIAN_FRONTEND=noninteractive
  DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=6 '
  DIRSTACK=()
  DISTRIBUTION=bookworm
  EUID=0
  FUNCNAME=([0]="Echo" [1]="main")
  GROUPS=()
  HOME=/root
  HOSTNAME=i-capture-the-hostname
  HOSTTYPE=arm
  HOST_ARCH=armhf
  IFS=' 	
  '
  INVOCATION_ID=6384943d34ec4d459bce79499e3fcdff
  LANG=C
  LANGUAGE=it_CH:it
  LC_ALL=C
  MACHTYPE=arm-unknown-linux-gnueabihf
  MAIL=/var/mail/root
  OPTERR=1
  OPTIND=1
  OSTYPE=linux-gnueabihf
  PATH=/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/i/capture/the/path
  PBCURRENTCOMMANDLINEOPERATION=build
  PBUILDER_OPERATION=build
  PBUILDER_PKGDATADIR=/usr/share/pbuilder
  PBUILDER_PKGLIBDIR=/usr/lib/pbuilder
  PBUILDER_SYSCONFDIR=/etc
  PIPESTATUS=([0]="0")
  POSIXLY_CORRECT=y
  PPID=21008
  PS4='+ '
  PWD=/
  SHELL=/bin/bash
  SHELLOPTS=braceexpand:errexit:hashall:interactive-comments:posix
  SHLVL=3
  SUDO_COMMAND='/usr/bin/timeout -k 24.1h 24h /usr/bin/ionice -c 3 /usr/bin/nice -n 11 /usr/bin/unshare --uts -- /usr/sbin/pbuilder --build --configfile /srv/reproducible-results/rbuild-debian/r-b-build.DadMrFO3/pbuilderrc_Ry3P --distribution bookworm --hookdir /etc/pbuilder/rebuild-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/bookworm-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/r-b-build.DadMrFO3/b2 --logfile b2/build.log --extrapackages usrmerge coq-unicoq_1.6-8.16-2.dsc'
  SUDO_GID=114
  SUDO_UID=109
  SUDO_USER=jenkins
  TERM=unknown
  TZ=/usr/share/zoneinfo/Etc/GMT-14
  UID=0
  USER=root
  _='I: set'
  http_proxy=http://10.0.0.15:3142/
I: uname -a
  Linux i-capture-the-hostname 5.10.0-23-arm64 #1 SMP Debian 5.10.179-1 (2023-05-12) aarch64 GNU/Linux
I: ls -l /bin
  total 5072
  -rwxr-xr-x 1 root root 838488 Apr 24 11:24 bash
  -rwxr-xr-x 3 root root  67144 Sep 19  2022 bunzip2
  -rwxr-xr-x 3 root root  67144 Sep 19  2022 bzcat
  lrwxrwxrwx 1 root root      6 Sep 19  2022 bzcmp -> bzdiff
  -rwxr-xr-x 1 root root   2225 Sep 19  2022 bzdiff
  lrwxrwxrwx 1 root root      6 Sep 19  2022 bzegrep -> bzgrep
  -rwxr-xr-x 1 root root   4893 Nov 28  2021 bzexe
  lrwxrwxrwx 1 root root      6 Sep 19  2022 bzfgrep -> bzgrep
  -rwxr-xr-x 1 root root   3775 Sep 19  2022 bzgrep
  -rwxr-xr-x 3 root root  67144 Sep 19  2022 bzip2
  -rwxr-xr-x 1 root root  67112 Sep 19  2022 bzip2recover
  lrwxrwxrwx 1 root root      6 Sep 19  2022 bzless -> bzmore
  -rwxr-xr-x 1 root root   1297 Sep 19  2022 bzmore
  -rwxr-xr-x 1 root root  67632 Sep 21  2022 cat
  -rwxr-xr-x 1 root root  67676 Sep 21  2022 chgrp
  -rwxr-xr-x 1 root root  67644 Sep 21  2022 chmod
  -rwxr-xr-x 1 root root  67684 Sep 21  2022 chown
  -rwxr-xr-x 1 root root 133532 Sep 21  2022 cp
  -rwxr-xr-x 1 root root 132868 Jan  6 03:20 dash
  -rwxr-xr-x 1 root root 133220 Sep 21  2022 date
  -rwxr-xr-x 1 root root  67732 Sep 21  2022 dd
  -rwxr-xr-x 1 root root  68104 Sep 21  2022 df
  -rwxr-xr-x 1 root root 133632 Sep 21  2022 dir
  -rwxr-xr-x 1 root root  59128 Mar 23 23:02 dmesg
  lrwxrwxrwx 1 root root      8 Dec 20 03:33 dnsdomainname -> hostname
  lrwxrwxrwx 1 root root      8 Dec 20 03:33 domainname -> hostname
  -rwxr-xr-x 1 root root  67560 Sep 21  2022 echo
  -rwxr-xr-x 1 root root     41 Jan 25 04:43 egrep
  -rwxr-xr-x 1 root root  67548 Sep 21  2022 false
  -rwxr-xr-x 1 root root     41 Jan 25 04:43 fgrep
  -rwxr-xr-x 1 root root  55748 Mar 23 23:02 findmnt
  -rwsr-xr-x 1 root root  26208 Mar 23 22:15 fusermount
  -rwxr-xr-x 1 root root 128608 Jan 25 04:43 grep
  -rwxr-xr-x 2 root root   2346 Apr 10  2022 gunzip
  -rwxr-xr-x 1 root root   6447 Apr 10  2022 gzexe
  -rwxr-xr-x 1 root root  64220 Apr 10  2022 gzip
  -rwxr-xr-x 1 root root  67032 Dec 20 03:33 hostname
  -rwxr-xr-x 1 root root  67720 Sep 21  2022 ln
  -rwxr-xr-x 1 root root  35132 Mar 23 23:51 login
  -rwxr-xr-x 1 root root 133632 Sep 21  2022 ls
  -rwxr-xr-x 1 root root 136808 Mar 23 23:02 lsblk
  -rwxr-xr-x 1 root root  67800 Sep 21  2022 mkdir
  -rwxr-xr-x 1 root root  67764 Sep 21  2022 mknod
  -rwxr-xr-x 1 root root  67596 Sep 21  2022 mktemp
  -rwxr-xr-x 1 root root  38504 Mar 23 23:02 more
  -rwsr-xr-x 1 root root  38496 Mar 23 23:02 mount
  -rwxr-xr-x 1 root root   9824 Mar 23 23:02 mountpoint
  -rwxr-xr-x 1 root root 133532 Sep 21  2022 mv
  lrwxrwxrwx 1 root root      8 Dec 20 03:33 nisdomainname -> hostname
  lrwxrwxrwx 1 root root     14 Apr  3 20:25 pidof -> /sbin/killall5
  -rwxr-xr-x 1 root root  67608 Sep 21  2022 pwd
  lrwxrwxrwx 1 root root      4 Apr 24 11:24 rbash -> bash
  -rwxr-xr-x 1 root root  67600 Sep 21  2022 readlink
  -rwxr-xr-x 1 root root  67672 Sep 21  2022 rm
  -rwxr-xr-x 1 root root  67600 Sep 21  2022 rmdir
  -rwxr-xr-x 1 root root  67400 Nov  3  2022 run-parts
  -rwxr-xr-x 1 root root 133372 Jan  6 09:55 sed
  lrwxrwxrwx 1 root root      9 May 30 23:07 sh -> /bin/bash
  -rwxr-xr-x 1 root root  67584 Sep 21  2022 sleep
  -rwxr-xr-x 1 root root  67644 Sep 21  2022 stty
  -rwsr-xr-x 1 root root  50800 Mar 23 23:02 su
  -rwxr-xr-x 1 root root  67584 Sep 21  2022 sync
  -rwxr-xr-x 1 root root 336764 Apr  7 04:25 tar
  -rwxr-xr-x 1 root root  67144 Nov  3  2022 tempfile
  -rwxr-xr-x 1 root root 133224 Sep 21  2022 touch
  -rwxr-xr-x 1 root root  67548 Sep 21  2022 true
  -rwxr-xr-x 1 root root   9768 Mar 23 22:15 ulockmgr_server
  -rwsr-xr-x 1 root root  22108 Mar 23 23:02 umount
  -rwxr-xr-x 1 root root  67572 Sep 21  2022 uname
  -rwxr-xr-x 2 root root   2346 Apr 10  2022 uncompress
  -rwxr-xr-x 1 root root 133632 Sep 21  2022 vdir
  -rwxr-xr-x 1 root root  42608 Mar 23 23:02 wdctl
  lrwxrwxrwx 1 root root      8 Dec 20 03:33 ypdomainname -> hostname
  -rwxr-xr-x 1 root root   1984 Apr 10  2022 zcat
  -rwxr-xr-x 1 root root   1678 Apr 10  2022 zcmp
  -rwxr-xr-x 1 root root   6460 Apr 10  2022 zdiff
  -rwxr-xr-x 1 root root     29 Apr 10  2022 zegrep
  -rwxr-xr-x 1 root root     29 Apr 10  2022 zfgrep
  -rwxr-xr-x 1 root root   2081 Apr 10  2022 zforce
  -rwxr-xr-x 1 root root   8103 Apr 10  2022 zgrep
  -rwxr-xr-x 1 root root   2206 Apr 10  2022 zless
  -rwxr-xr-x 1 root root   1842 Apr 10  2022 zmore
  -rwxr-xr-x 1 root root   4577 Apr 10  2022 znew
I: user script /srv/workspace/pbuilder/21008/tmp/hooks/D02_print_environment finished
 -> Attempting to satisfy build-dependencies
 -> Creating pbuilder-satisfydepends-dummy package
Package: pbuilder-satisfydepends-dummy
Version: 0.invalid.0
Architecture: armhf
Maintainer: Debian Pbuilder Team <pbuilder-maint@lists.alioth.debian.org>
Description: Dummy package to satisfy dependencies with aptitude - created by pbuilder
 This package was created automatically by pbuilder to satisfy the
 build-dependencies of the package being currently built.
Depends: coq, debhelper-compat (= 13), dh-coq, dh-ocaml, libcoq-core-ocaml-dev, libcoq-stdlib
dpkg-deb: building package 'pbuilder-satisfydepends-dummy' in '/tmp/satisfydepends-aptitude/pbuilder-satisfydepends-dummy.deb'.
Selecting previously unselected package pbuilder-satisfydepends-dummy.
(Reading database ... 19324 files and directories currently installed.)
Preparing to unpack .../pbuilder-satisfydepends-dummy.deb ...
Unpacking pbuilder-satisfydepends-dummy (0.invalid.0) ...
dpkg: pbuilder-satisfydepends-dummy: dependency problems, but configuring anyway as you requested:
 pbuilder-satisfydepends-dummy depends on coq; however:
  Package coq is not installed.
 pbuilder-satisfydepends-dummy depends on debhelper-compat (= 13); however:
  Package debhelper-compat is not installed.
 pbuilder-satisfydepends-dummy depends on dh-coq; however:
  Package dh-coq is not installed.
 pbuilder-satisfydepends-dummy depends on dh-ocaml; however:
  Package dh-ocaml is not installed.
 pbuilder-satisfydepends-dummy depends on libcoq-core-ocaml-dev; however:
  Package libcoq-core-ocaml-dev is not installed.
 pbuilder-satisfydepends-dummy depends on libcoq-stdlib; however:
  Package libcoq-stdlib is not installed.

Setting up pbuilder-satisfydepends-dummy (0.invalid.0) ...
Reading package lists...
Building dependency tree...
Reading state information...
Initializing package states...
Writing extended state information...
Building tag database...
pbuilder-satisfydepends-dummy is already installed at the requested version (0.invalid.0)
pbuilder-satisfydepends-dummy is already installed at the requested version (0.invalid.0)
The following NEW packages will be installed:
  autoconf{a} automake{a} autopoint{a} autotools-dev{a} bsdextrautils{a} coq{a} debhelper{a} dh-autoreconf{a} dh-coq{a} dh-ocaml{a} dh-strip-nondeterminism{a} dwz{a} file{a} gettext{a} gettext-base{a} groff-base{a} intltool-debian{a} libarchive-zip-perl{a} libcoq-core-ocaml{a} libcoq-core-ocaml-dev{a} libcoq-stdlib{a} libdebhelper-perl{a} libelf1{a} libexpat1{a} libfile-stripnondeterminism-perl{a} libfindlib-ocaml{a} libfindlib-ocaml-dev{a} libgmp-dev{a} libgmp3-dev{a} libgmpxx4ldbl{a} libicu72{a} libmagic-mgc{a} libmagic1{a} libncurses-dev{a} libncurses6{a} libpipeline1{a} libpython3-stdlib{a} libpython3.11-minimal{a} libpython3.11-stdlib{a} libreadline8{a} libsub-override-perl{a} libtool{a} libuchardet0{a} libxml2{a} libzarith-ocaml{a} libzarith-ocaml-dev{a} m4{a} man-db{a} media-types{a} ocaml{a} ocaml-base{a} ocaml-compiler-libs{a} ocaml-findlib{a} ocaml-interp{a} ocaml-nox{a} po-debconf{a} python3{a} python3-minimal{a} python3.11{a} python3.11-minimal{a} readline-common{a} sensible-utils{a} 
The following packages are RECOMMENDED but will NOT be installed:
  ca-certificates curl ledit libarchive-cpio-perl libgpm2 libltdl-dev libmail-sendmail-perl lynx ocaml-man rlfe rlwrap wget 
0 packages upgraded, 62 newly installed, 0 to remove and 0 not upgraded.
Need to get 310 MB of archives. After unpacking 1188 MB will be used.
Writing extended state information...
Get: 1 http://deb.debian.org/debian bookworm/main armhf libpython3.11-minimal armhf 3.11.2-6 [798 kB]
Get: 2 http://deb.debian.org/debian bookworm/main armhf libexpat1 armhf 2.5.0-1 [79.9 kB]
Get: 3 http://deb.debian.org/debian bookworm/main armhf python3.11-minimal armhf 3.11.2-6 [1714 kB]
Get: 4 http://deb.debian.org/debian bookworm/main armhf python3-minimal armhf 3.11.2-1+b1 [26.3 kB]
Get: 5 http://deb.debian.org/debian bookworm/main armhf media-types all 10.0.0 [26.1 kB]
Get: 6 http://deb.debian.org/debian bookworm/main armhf readline-common all 8.2-1.3 [69.0 kB]
Get: 7 http://deb.debian.org/debian bookworm/main armhf libreadline8 armhf 8.2-1.3 [144 kB]
Get: 8 http://deb.debian.org/debian bookworm/main armhf libpython3.11-stdlib armhf 3.11.2-6 [1678 kB]
Get: 9 http://deb.debian.org/debian bookworm/main armhf python3.11 armhf 3.11.2-6 [572 kB]
Get: 10 http://deb.debian.org/debian bookworm/main armhf libpython3-stdlib armhf 3.11.2-1+b1 [9296 B]
Get: 11 http://deb.debian.org/debian bookworm/main armhf python3 armhf 3.11.2-1+b1 [26.3 kB]
Get: 12 http://deb.debian.org/debian bookworm/main armhf sensible-utils all 0.0.17+nmu1 [19.0 kB]
Get: 13 http://deb.debian.org/debian bookworm/main armhf libmagic-mgc armhf 1:5.44-3 [305 kB]
Get: 14 http://deb.debian.org/debian bookworm/main armhf libmagic1 armhf 1:5.44-3 [96.5 kB]
Get: 15 http://deb.debian.org/debian bookworm/main armhf file armhf 1:5.44-3 [41.6 kB]
Get: 16 http://deb.debian.org/debian bookworm/main armhf gettext-base armhf 0.21-12 [157 kB]
Get: 17 http://deb.debian.org/debian bookworm/main armhf libuchardet0 armhf 0.0.7-1 [65.0 kB]
Get: 18 http://deb.debian.org/debian bookworm/main armhf groff-base armhf 1.22.4-10 [825 kB]
Get: 19 http://deb.debian.org/debian bookworm/main armhf bsdextrautils armhf 2.38.1-5+b1 [78.6 kB]
Get: 20 http://deb.debian.org/debian bookworm/main armhf libpipeline1 armhf 1.5.7-1 [33.6 kB]
Get: 21 http://deb.debian.org/debian bookworm/main armhf man-db armhf 2.11.2-2 [1351 kB]
Get: 22 http://deb.debian.org/debian bookworm/main armhf m4 armhf 1.4.19-3 [265 kB]
Get: 23 http://deb.debian.org/debian bookworm/main armhf autoconf all 2.71-3 [332 kB]
Get: 24 http://deb.debian.org/debian bookworm/main armhf autotools-dev all 20220109.1 [51.6 kB]
Get: 25 http://deb.debian.org/debian bookworm/main armhf automake all 1:1.16.5-1.3 [823 kB]
Get: 26 http://deb.debian.org/debian bookworm/main armhf autopoint all 0.21-12 [495 kB]
Get: 27 http://deb.debian.org/debian bookworm/main armhf libcoq-stdlib armhf 8.16.1+dfsg-1+b2 [21.5 MB]
Get: 28 http://deb.debian.org/debian bookworm/main armhf ocaml-base armhf 4.13.1-4 [587 kB]
Get: 29 http://deb.debian.org/debian bookworm/main armhf libfindlib-ocaml armhf 1.9.6-1+b1 [167 kB]
Get: 30 http://deb.debian.org/debian bookworm/main armhf libzarith-ocaml armhf 1.12-1+b1 [52.3 kB]
Get: 31 http://deb.debian.org/debian bookworm/main armhf libcoq-core-ocaml armhf 8.16.1+dfsg-1+b2 [22.3 MB]
Get: 32 http://deb.debian.org/debian bookworm/main armhf ocaml-compiler-libs armhf 4.13.1-4 [29.5 MB]
Get: 33 http://deb.debian.org/debian bookworm/main armhf ocaml-interp armhf 4.13.1-4 [6158 kB]
Get: 34 http://deb.debian.org/debian bookworm/main armhf libncurses6 armhf 6.4-4 [81.1 kB]
Get: 35 http://deb.debian.org/debian bookworm/main armhf libncurses-dev armhf 6.4-4 [311 kB]
Get: 36 http://deb.debian.org/debian bookworm/main armhf ocaml armhf 4.13.1-4 [71.3 MB]
Get: 37 http://deb.debian.org/debian bookworm/main armhf ocaml-nox all 4.13.1-4 [161 kB]
Get: 38 http://deb.debian.org/debian bookworm/main armhf ocaml-findlib armhf 1.9.6-1+b1 [454 kB]
Get: 39 http://deb.debian.org/debian bookworm/main armhf coq armhf 8.16.1+dfsg-1+b2 [89.9 MB]
Get: 40 http://deb.debian.org/debian bookworm/main armhf libdebhelper-perl all 13.11.4 [81.2 kB]
Get: 41 http://deb.debian.org/debian bookworm/main armhf libtool all 2.4.7-5 [517 kB]
Get: 42 http://deb.debian.org/debian bookworm/main armhf dh-autoreconf all 20 [17.1 kB]
Get: 43 http://deb.debian.org/debian bookworm/main armhf libarchive-zip-perl all 1.68-1 [104 kB]
Get: 44 http://deb.debian.org/debian bookworm/main armhf libsub-override-perl all 0.09-4 [9304 B]
Get: 45 http://deb.debian.org/debian bookworm/main armhf libfile-stripnondeterminism-perl all 1.13.1-1 [19.4 kB]
Get: 46 http://deb.debian.org/debian bookworm/main armhf dh-strip-nondeterminism all 1.13.1-1 [8620 B]
Get: 47 http://deb.debian.org/debian bookworm/main armhf libelf1 armhf 0.188-2.1 [170 kB]
Get: 48 http://deb.debian.org/debian bookworm/main armhf dwz armhf 0.15-1 [101 kB]
Get: 49 http://deb.debian.org/debian bookworm/main armhf libicu72 armhf 72.1-3 [9048 kB]
Get: 50 http://deb.debian.org/debian bookworm/main armhf libxml2 armhf 2.9.14+dfsg-1.2 [591 kB]
Get: 51 http://deb.debian.org/debian bookworm/main armhf gettext armhf 0.21-12 [1229 kB]
Get: 52 http://deb.debian.org/debian bookworm/main armhf intltool-debian all 0.35.0+20060710.6 [22.9 kB]
Get: 53 http://deb.debian.org/debian bookworm/main armhf po-debconf all 1.0.21+nmu1 [248 kB]
Get: 54 http://deb.debian.org/debian bookworm/main armhf debhelper all 13.11.4 [942 kB]
Get: 55 http://deb.debian.org/debian bookworm/main armhf dh-coq all 0.5 [7460 B]
Get: 56 http://deb.debian.org/debian bookworm/main armhf dh-ocaml all 1.1.3 [82.9 kB]
Get: 57 http://deb.debian.org/debian bookworm/main armhf libfindlib-ocaml-dev armhf 1.9.6-1+b1 [164 kB]
Get: 58 http://deb.debian.org/debian bookworm/main armhf libgmpxx4ldbl armhf 2:6.2.1+dfsg1-1.1 [338 kB]
Get: 59 http://deb.debian.org/debian bookworm/main armhf libgmp-dev armhf 2:6.2.1+dfsg1-1.1 [593 kB]
Get: 60 http://deb.debian.org/debian bookworm/main armhf libgmp3-dev armhf 2:6.2.1+dfsg1-1.1 [331 kB]
Get: 61 http://deb.debian.org/debian bookworm/main armhf libzarith-ocaml-dev armhf 1.12-1+b1 [90.2 kB]
Get: 62 http://deb.debian.org/debian bookworm/main armhf libcoq-core-ocaml-dev armhf 8.16.1+dfsg-1+b2 [43.1 MB]
Fetched 310 MB in 28s (11.2 MB/s)
debconf: delaying package configuration, since apt-utils is not installed
Selecting previously unselected package libpython3.11-minimal:armhf.
(Reading database ... 
(Reading database ... 5%
(Reading database ... 10%
(Reading database ... 15%
(Reading database ... 20%
(Reading database ... 25%
(Reading database ... 30%
(Reading database ... 35%
(Reading database ... 40%
(Reading database ... 45%
(Reading database ... 50%
(Reading database ... 55%
(Reading database ... 60%
(Reading database ... 65%
(Reading database ... 70%
(Reading database ... 75%
(Reading database ... 80%
(Reading database ... 85%
(Reading database ... 90%
(Reading database ... 95%
(Reading database ... 100%
(Reading database ... 19324 files and directories currently installed.)
Preparing to unpack .../libpython3.11-minimal_3.11.2-6_armhf.deb ...
Unpacking libpython3.11-minimal:armhf (3.11.2-6) ...
Selecting previously unselected package libexpat1:armhf.
Preparing to unpack .../libexpat1_2.5.0-1_armhf.deb ...
Unpacking libexpat1:armhf (2.5.0-1) ...
Selecting previously unselected package python3.11-minimal.
Preparing to unpack .../python3.11-minimal_3.11.2-6_armhf.deb ...
Unpacking python3.11-minimal (3.11.2-6) ...
Setting up libpython3.11-minimal:armhf (3.11.2-6) ...
Setting up libexpat1:armhf (2.5.0-1) ...
Setting up python3.11-minimal (3.11.2-6) ...
Selecting previously unselected package python3-minimal.
(Reading database ... 
(Reading database ... 5%
(Reading database ... 10%
(Reading database ... 15%
(Reading database ... 20%
(Reading database ... 25%
(Reading database ... 30%
(Reading database ... 35%
(Reading database ... 40%
(Reading database ... 45%
(Reading database ... 50%
(Reading database ... 55%
(Reading database ... 60%
(Reading database ... 65%
(Reading database ... 70%
(Reading database ... 75%
(Reading database ... 80%
(Reading database ... 85%
(Reading database ... 90%
(Reading database ... 95%
(Reading database ... 100%
(Reading database ... 19640 files and directories currently installed.)
Preparing to unpack .../0-python3-minimal_3.11.2-1+b1_armhf.deb ...
Unpacking python3-minimal (3.11.2-1+b1) ...
Selecting previously unselected package media-types.
Preparing to unpack .../1-media-types_10.0.0_all.deb ...
Unpacking media-types (10.0.0) ...
Selecting previously unselected package readline-common.
Preparing to unpack .../2-readline-common_8.2-1.3_all.deb ...
Unpacking readline-common (8.2-1.3) ...
Selecting previously unselected package libreadline8:armhf.
Preparing to unpack .../3-libreadline8_8.2-1.3_armhf.deb ...
Unpacking libreadline8:armhf (8.2-1.3) ...
Selecting previously unselected package libpython3.11-stdlib:armhf.
Preparing to unpack .../4-libpython3.11-stdlib_3.11.2-6_armhf.deb ...
Unpacking libpython3.11-stdlib:armhf (3.11.2-6) ...
Selecting previously unselected package python3.11.
Preparing to unpack .../5-python3.11_3.11.2-6_armhf.deb ...
Unpacking python3.11 (3.11.2-6) ...
Selecting previously unselected package libpython3-stdlib:armhf.
Preparing to unpack .../6-libpython3-stdlib_3.11.2-1+b1_armhf.deb ...
Unpacking libpython3-stdlib:armhf (3.11.2-1+b1) ...
Setting up python3-minimal (3.11.2-1+b1) ...
Selecting previously unselected package python3.
(Reading database ... 
(Reading database ... 5%
(Reading database ... 10%
(Reading database ... 15%
(Reading database ... 20%
(Reading database ... 25%
(Reading database ... 30%
(Reading database ... 35%
(Reading database ... 40%
(Reading database ... 45%
(Reading database ... 50%
(Reading database ... 55%
(Reading database ... 60%
(Reading database ... 65%
(Reading database ... 70%
(Reading database ... 75%
(Reading database ... 80%
(Reading database ... 85%
(Reading database ... 90%
(Reading database ... 95%
(Reading database ... 100%
(Reading database ... 20074 files and directories currently installed.)
Preparing to unpack .../00-python3_3.11.2-1+b1_armhf.deb ...
Unpacking python3 (3.11.2-1+b1) ...
Selecting previously unselected package sensible-utils.
Preparing to unpack .../01-sensible-utils_0.0.17+nmu1_all.deb ...
Unpacking sensible-utils (0.0.17+nmu1) ...
Selecting previously unselected package libmagic-mgc.
Preparing to unpack .../02-libmagic-mgc_1%3a5.44-3_armhf.deb ...
Unpacking libmagic-mgc (1:5.44-3) ...
Selecting previously unselected package libmagic1:armhf.
Preparing to unpack .../03-libmagic1_1%3a5.44-3_armhf.deb ...
Unpacking libmagic1:armhf (1:5.44-3) ...
Selecting previously unselected package file.
Preparing to unpack .../04-file_1%3a5.44-3_armhf.deb ...
Unpacking file (1:5.44-3) ...
Selecting previously unselected package gettext-base.
Preparing to unpack .../05-gettext-base_0.21-12_armhf.deb ...
Unpacking gettext-base (0.21-12) ...
Selecting previously unselected package libuchardet0:armhf.
Preparing to unpack .../06-libuchardet0_0.0.7-1_armhf.deb ...
Unpacking libuchardet0:armhf (0.0.7-1) ...
Selecting previously unselected package groff-base.
Preparing to unpack .../07-groff-base_1.22.4-10_armhf.deb ...
Unpacking groff-base (1.22.4-10) ...
Selecting previously unselected package bsdextrautils.
Preparing to unpack .../08-bsdextrautils_2.38.1-5+b1_armhf.deb ...
Unpacking bsdextrautils (2.38.1-5+b1) ...
Selecting previously unselected package libpipeline1:armhf.
Preparing to unpack .../09-libpipeline1_1.5.7-1_armhf.deb ...
Unpacking libpipeline1:armhf (1.5.7-1) ...
Selecting previously unselected package man-db.
Preparing to unpack .../10-man-db_2.11.2-2_armhf.deb ...
Unpacking man-db (2.11.2-2) ...
Selecting previously unselected package m4.
Preparing to unpack .../11-m4_1.4.19-3_armhf.deb ...
Unpacking m4 (1.4.19-3) ...
Selecting previously unselected package autoconf.
Preparing to unpack .../12-autoconf_2.71-3_all.deb ...
Unpacking autoconf (2.71-3) ...
Selecting previously unselected package autotools-dev.
Preparing to unpack .../13-autotools-dev_20220109.1_all.deb ...
Unpacking autotools-dev (20220109.1) ...
Selecting previously unselected package automake.
Preparing to unpack .../14-automake_1%3a1.16.5-1.3_all.deb ...
Unpacking automake (1:1.16.5-1.3) ...
Selecting previously unselected package autopoint.
Preparing to unpack .../15-autopoint_0.21-12_all.deb ...
Unpacking autopoint (0.21-12) ...
Selecting previously unselected package libcoq-stdlib.
Preparing to unpack .../16-libcoq-stdlib_8.16.1+dfsg-1+b2_armhf.deb ...
Unpacking libcoq-stdlib (8.16.1+dfsg-1+b2) ...
Selecting previously unselected package ocaml-base.
Preparing to unpack .../17-ocaml-base_4.13.1-4_armhf.deb ...
Unpacking ocaml-base (4.13.1-4) ...
Selecting previously unselected package libfindlib-ocaml.
Preparing to unpack .../18-libfindlib-ocaml_1.9.6-1+b1_armhf.deb ...
Unpacking libfindlib-ocaml (1.9.6-1+b1) ...
Selecting previously unselected package libzarith-ocaml.
Preparing to unpack .../19-libzarith-ocaml_1.12-1+b1_armhf.deb ...
Unpacking libzarith-ocaml (1.12-1+b1) ...
Selecting previously unselected package libcoq-core-ocaml.
Preparing to unpack .../20-libcoq-core-ocaml_8.16.1+dfsg-1+b2_armhf.deb ...
Unpacking libcoq-core-ocaml (8.16.1+dfsg-1+b2) ...
Selecting previously unselected package ocaml-compiler-libs.
Preparing to unpack .../21-ocaml-compiler-libs_4.13.1-4_armhf.deb ...
Unpacking ocaml-compiler-libs (4.13.1-4) ...
Selecting previously unselected package ocaml-interp.
Preparing to unpack .../22-ocaml-interp_4.13.1-4_armhf.deb ...
Unpacking ocaml-interp (4.13.1-4) ...
Selecting previously unselected package libncurses6:armhf.
Preparing to unpack .../23-libncurses6_6.4-4_armhf.deb ...
Unpacking libncurses6:armhf (6.4-4) ...
Selecting previously unselected package libncurses-dev:armhf.
Preparing to unpack .../24-libncurses-dev_6.4-4_armhf.deb ...
Unpacking libncurses-dev:armhf (6.4-4) ...
Selecting previously unselected package ocaml.
Preparing to unpack .../25-ocaml_4.13.1-4_armhf.deb ...
Unpacking ocaml (4.13.1-4) ...
Selecting previously unselected package ocaml-nox.
Preparing to unpack .../26-ocaml-nox_4.13.1-4_all.deb ...
Unpacking ocaml-nox (4.13.1-4) ...
Selecting previously unselected package ocaml-findlib.
Preparing to unpack .../27-ocaml-findlib_1.9.6-1+b1_armhf.deb ...
Unpacking ocaml-findlib (1.9.6-1+b1) ...
Selecting previously unselected package coq.
Preparing to unpack .../28-coq_8.16.1+dfsg-1+b2_armhf.deb ...
Unpacking coq (8.16.1+dfsg-1+b2) ...
Selecting previously unselected package libdebhelper-perl.
Preparing to unpack .../29-libdebhelper-perl_13.11.4_all.deb ...
Unpacking libdebhelper-perl (13.11.4) ...
Selecting previously unselected package libtool.
Preparing to unpack .../30-libtool_2.4.7-5_all.deb ...
Unpacking libtool (2.4.7-5) ...
Selecting previously unselected package dh-autoreconf.
Preparing to unpack .../31-dh-autoreconf_20_all.deb ...
Unpacking dh-autoreconf (20) ...
Selecting previously unselected package libarchive-zip-perl.
Preparing to unpack .../32-libarchive-zip-perl_1.68-1_all.deb ...
Unpacking libarchive-zip-perl (1.68-1) ...
Selecting previously unselected package libsub-override-perl.
Preparing to unpack .../33-libsub-override-perl_0.09-4_all.deb ...
Unpacking libsub-override-perl (0.09-4) ...
Selecting previously unselected package libfile-stripnondeterminism-perl.
Preparing to unpack .../34-libfile-stripnondeterminism-perl_1.13.1-1_all.deb ...
Unpacking libfile-stripnondeterminism-perl (1.13.1-1) ...
Selecting previously unselected package dh-strip-nondeterminism.
Preparing to unpack .../35-dh-strip-nondeterminism_1.13.1-1_all.deb ...
Unpacking dh-strip-nondeterminism (1.13.1-1) ...
Selecting previously unselected package libelf1:armhf.
Preparing to unpack .../36-libelf1_0.188-2.1_armhf.deb ...
Unpacking libelf1:armhf (0.188-2.1) ...
Selecting previously unselected package dwz.
Preparing to unpack .../37-dwz_0.15-1_armhf.deb ...
Unpacking dwz (0.15-1) ...
Selecting previously unselected package libicu72:armhf.
Preparing to unpack .../38-libicu72_72.1-3_armhf.deb ...
Unpacking libicu72:armhf (72.1-3) ...
Selecting previously unselected package libxml2:armhf.
Preparing to unpack .../39-libxml2_2.9.14+dfsg-1.2_armhf.deb ...
Unpacking libxml2:armhf (2.9.14+dfsg-1.2) ...
Selecting previously unselected package gettext.
Preparing to unpack .../40-gettext_0.21-12_armhf.deb ...
Unpacking gettext (0.21-12) ...
Selecting previously unselected package intltool-debian.
Preparing to unpack .../41-intltool-debian_0.35.0+20060710.6_all.deb ...
Unpacking intltool-debian (0.35.0+20060710.6) ...
Selecting previously unselected package po-debconf.
Preparing to unpack .../42-po-debconf_1.0.21+nmu1_all.deb ...
Unpacking po-debconf (1.0.21+nmu1) ...
Selecting previously unselected package debhelper.
Preparing to unpack .../43-debhelper_13.11.4_all.deb ...
Unpacking debhelper (13.11.4) ...
Selecting previously unselected package dh-coq.
Preparing to unpack .../44-dh-coq_0.5_all.deb ...
Unpacking dh-coq (0.5) ...
Selecting previously unselected package dh-ocaml.
Preparing to unpack .../45-dh-ocaml_1.1.3_all.deb ...
Unpacking dh-ocaml (1.1.3) ...
Selecting previously unselected package libfindlib-ocaml-dev.
Preparing to unpack .../46-libfindlib-ocaml-dev_1.9.6-1+b1_armhf.deb ...
Unpacking libfindlib-ocaml-dev (1.9.6-1+b1) ...
Selecting previously unselected package libgmpxx4ldbl:armhf.
Preparing to unpack .../47-libgmpxx4ldbl_2%3a6.2.1+dfsg1-1.1_armhf.deb ...
Unpacking libgmpxx4ldbl:armhf (2:6.2.1+dfsg1-1.1) ...
Selecting previously unselected package libgmp-dev:armhf.
Preparing to unpack .../48-libgmp-dev_2%3a6.2.1+dfsg1-1.1_armhf.deb ...
Unpacking libgmp-dev:armhf (2:6.2.1+dfsg1-1.1) ...
Selecting previously unselected package libgmp3-dev:armhf.
Preparing to unpack .../49-libgmp3-dev_2%3a6.2.1+dfsg1-1.1_armhf.deb ...
Unpacking libgmp3-dev:armhf (2:6.2.1+dfsg1-1.1) ...
Selecting previously unselected package libzarith-ocaml-dev.
Preparing to unpack .../50-libzarith-ocaml-dev_1.12-1+b1_armhf.deb ...
Unpacking libzarith-ocaml-dev (1.12-1+b1) ...
Selecting previously unselected package libcoq-core-ocaml-dev.
Preparing to unpack .../51-libcoq-core-ocaml-dev_8.16.1+dfsg-1+b2_armhf.deb ...
Unpacking libcoq-core-ocaml-dev (8.16.1+dfsg-1+b2) ...
Setting up media-types (10.0.0) ...
Setting up libpipeline1:armhf (1.5.7-1) ...
Setting up libicu72:armhf (72.1-3) ...
Setting up bsdextrautils (2.38.1-5+b1) ...
Setting up libmagic-mgc (1:5.44-3) ...
Setting up dh-coq (0.5) ...
Setting up libarchive-zip-perl (1.68-1) ...
Setting up libdebhelper-perl (13.11.4) ...
Setting up dh-ocaml (1.1.3) ...
Setting up libmagic1:armhf (1:5.44-3) ...
Setting up gettext-base (0.21-12) ...
Setting up m4 (1.4.19-3) ...
Setting up file (1:5.44-3) ...
Setting up autotools-dev (20220109.1) ...
Setting up libcoq-stdlib (8.16.1+dfsg-1+b2) ...
Setting up libgmpxx4ldbl:armhf (2:6.2.1+dfsg1-1.1) ...
Setting up libncurses6:armhf (6.4-4) ...
Setting up autopoint (0.21-12) ...
Setting up ocaml-base (4.13.1-4) ...
Setting up autoconf (2.71-3) ...
Setting up sensible-utils (0.0.17+nmu1) ...
Setting up libuchardet0:armhf (0.0.7-1) ...
Setting up libsub-override-perl (0.09-4) ...
Setting up libelf1:armhf (0.188-2.1) ...
Setting up readline-common (8.2-1.3) ...
Setting up libxml2:armhf (2.9.14+dfsg-1.2) ...
Setting up automake (1:1.16.5-1.3) ...
update-alternatives: using /usr/bin/automake-1.16 to provide /usr/bin/automake (automake) in auto mode
Setting up libfile-stripnondeterminism-perl (1.13.1-1) ...
Setting up libncurses-dev:armhf (6.4-4) ...
Setting up gettext (0.21-12) ...
Setting up libgmp-dev:armhf (2:6.2.1+dfsg1-1.1) ...
Setting up libtool (2.4.7-5) ...
Setting up libreadline8:armhf (8.2-1.3) ...
Setting up libfindlib-ocaml (1.9.6-1+b1) ...
Setting up libzarith-ocaml (1.12-1+b1) ...
Setting up intltool-debian (0.35.0+20060710.6) ...
Setting up dh-autoreconf (20) ...
Setting up ocaml-findlib (1.9.6-1+b1) ...
Setting up dh-strip-nondeterminism (1.13.1-1) ...
Setting up dwz (0.15-1) ...
Setting up libcoq-core-ocaml (8.16.1+dfsg-1+b2) ...
Setting up groff-base (1.22.4-10) ...
Setting up libgmp3-dev:armhf (2:6.2.1+dfsg1-1.1) ...
Setting up po-debconf (1.0.21+nmu1) ...
Setting up libpython3.11-stdlib:armhf (3.11.2-6) ...
Setting up man-db (2.11.2-2) ...
Not building database; man-db/auto-update is not 'true'.
Setting up libpython3-stdlib:armhf (3.11.2-1+b1) ...
Setting up python3.11 (3.11.2-6) ...
Setting up debhelper (13.11.4) ...
Setting up python3 (3.11.2-1+b1) ...
Setting up ocaml-compiler-libs (4.13.1-4) ...
Setting up ocaml-interp (4.13.1-4) ...
Setting up ocaml (4.13.1-4) ...
Setting up libfindlib-ocaml-dev (1.9.6-1+b1) ...
Setting up ocaml-nox (4.13.1-4) ...
Setting up coq (8.16.1+dfsg-1+b2) ...
Setting up libzarith-ocaml-dev (1.12-1+b1) ...
Setting up libcoq-core-ocaml-dev (8.16.1+dfsg-1+b2) ...
Processing triggers for libc-bin (2.36-9) ...
Reading package lists...
Building dependency tree...
Reading state information...
Reading extended state information...
Initializing package states...
Writing extended state information...
Building tag database...
 -> Finished parsing the build-deps
Reading package lists...
Building dependency tree...
Reading state information...
usrmerge is already the newest version (35).
0 upgraded, 0 newly installed, 0 to remove and 0 not upgraded.
I: Building the package
I: user script /srv/workspace/pbuilder/21008/tmp/hooks/A99_set_merged_usr starting
Re-configuring usrmerge...
removed '/etc/unsupported-skip-usrmerge-conversion'
The system has been successfully converted.
I: user script /srv/workspace/pbuilder/21008/tmp/hooks/A99_set_merged_usr finished
hostname: Name or service not known
I: Running cd /build/coq-unicoq-1.6-8.16/ && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/i/capture/the/path" HOME="/nonexistent/second-build" dpkg-buildpackage -us -uc -b && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/i/capture/the/path" HOME="/nonexistent/second-build" dpkg-genchanges -S  > ../coq-unicoq_1.6-8.16-2_source.changes
dpkg-buildpackage: info: source package coq-unicoq
dpkg-buildpackage: info: source version 1.6-8.16-2
dpkg-buildpackage: info: source distribution unstable
dpkg-buildpackage: info: source changed by Julien Puydt <jpuydt@debian.org>
 dpkg-source --before-build .
dpkg-buildpackage: info: host architecture armhf
 debian/rules clean
dh clean --with coq,ocaml
   debian/rules override_dh_auto_clean
make[1]: Entering directory '/build/coq-unicoq-1.6-8.16'
Doesn't work as expected
make[1]: Leaving directory '/build/coq-unicoq-1.6-8.16'
   dh_ocamlclean
   dh_clean
 debian/rules binary
dh binary --with coq,ocaml
   dh_update_autotools_config
   dh_autoreconf
   dh_ocamlinit
   debian/rules override_dh_auto_configure
make[1]: Entering directory '/build/coq-unicoq-1.6-8.16'
coq_makefile -f _CoqProject -o Makefile
make[1]: Leaving directory '/build/coq-unicoq-1.6-8.16'
   dh_auto_build
	make -j6 "INSTALL=install --strip-program=true"
make[1]: Entering directory '/build/coq-unicoq-1.6-8.16'
COQDEP VFILES
COQPP src/unitactics.mlg
CAMLDEP src/munify.mli
CAMLDEP src/logger.mli
OCAMLLIBDEP src/unicoq.mlpack
CAMLDEP src/munify.ml
CAMLDEP src/logger.ml
CAMLDEP src/unitactics.ml
CAMLC -c src/logger.mli
CAMLOPT -c -for-pack Unicoq src/logger.ml
CAMLC -c src/munify.mli
CAMLOPT -c -for-pack Unicoq src/munify.ml
File "src/munify.ml", line 670, characters 8-32:
670 |         Termops.global_of_constr sigma t1, l1
              ^^^^^^^^^^^^^^^^^^^^^^^^
Alert deprecated: Termops.global_of_constr
Use [EConstr.destRef] instead (throws DestKO instead of Not_found).
File "src/munify.ml", line 690, characters 25-49:
690 |               let c2,_ = Termops.global_of_constr sigma t2 in
                               ^^^^^^^^^^^^^^^^^^^^^^^^
Alert deprecated: Termops.global_of_constr
Use [EConstr.destRef] instead (throws DestKO instead of Not_found).
File "src/munify.ml", line 1210, characters 38-52:
1210 |     | Const (c1,_), Const (c2,_) when Constant.equal c1 c2 ->
                                             ^^^^^^^^^^^^^^
Alert deprecated: Names.Constant.equal
Use QConstant.equal
File "src/munify.ml", line 1214, characters 34-46:
1214 |     | Ind (c1,_), Ind (c2,_) when Names.eq_ind c1 c2 ->
                                         ^^^^^^^^^^^^
Alert deprecated: Names.eq_ind
Use the Ind module
File "src/munify.ml", line 1218, characters 46-66:
1218 |     | Construct (c1,_), Construct (c2,_) when Names.eq_constructor c1 c2 ->
                                                     ^^^^^^^^^^^^^^^^^^^^
Alert deprecated: Names.eq_constructor
Use the Construct module
File "src/munify.ml", line 1223, characters 40-67:
1223 |     | Proj (c1, t1), Proj (c2, t2) when Names.Projection.repr_equal c1 c2 ->
                                               ^^^^^^^^^^^^^^^^^^^^^^^^^^^
Alert deprecated: Names.Projection.repr_equal
Use an explicit projection of Repr
CAMLOPT -c -for-pack Unicoq src/unitactics.ml
CAMLOPT -pack -o src/unicoq.cmx
CAMLOPT -a -o src/unicoq.cmxa
CAMLOPT -shared -o src/unicoq.cmxs
COQC theories/Unicoq.v
COQC test-suite/munifytest.v
COQC test-suite/microtests.v
COQC test-suite/primitive.v
COQC test-suite/instantiate.v
COQC test-suite/timings.v
COQC test-suite/bug_41.v
STATS:	0		0
?A =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
(nat -> nat) =<= nat (App-FO) ERR
(nat -> nat) =<= nat (App-FO) ERR
(?x = ?x) =<= ((?n : nat -> nat) 0 = 1) (App-FO) OK
_@eq =<= @eq (Rigid-Same) OK
_?A =?= nat (Meta-Inst) OK
__Set =<= Type (Reduce-Same) OK
_?x =?= (?n 0) (Meta-Inst) OK
__nat =<= nat (Reduce-Same) OK
_(?n 0) =?= 1 (Meta-FO) OK
__?n =?= S (Meta-Inst) OK
___(nat -> nat) =<= (nat -> nat) (Reduce-Same) OK
__0 =?= 0 (Reduce-Same) OK
?A =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same)Decimal.uint =<= Decimal.uint (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Number.uint =<= Number.uint (Reduce-Same)
?T =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
?T@\{x:=x; x0:=x\} =<= ?A (Meta-Inst)
_?A =<= ?T@\{x:=x; x0:=x\} (Meta-Inst)
?T@\{x:=x; x0:=x\} =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Number.uint =<= Number.uint (Reduce-Same)
?A =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
nat =<= nat (Reduce-Same)
nat =<= nat (Reduce-Same)
nat =<= nat (Reduce-Same)
nat =<= nat (Reduce-Same)
nat =<= nat (Reduce-Same)
nat =<= nat (Reduce-Same)
(0 = 0) =<= (?n x = 0) (App-FO)
_@eq =<= @eq (Rigid-Same)
_nat =?= nat (Reduce-Same)
nat =<= nat (Reduce-Same)
nat =<= nat (Reduce-Same)
_(?n x) =?= 0 (Meta-Inst)
__(nat -> nat) =<= (nat -> nat) (Reduce-Same)
nat =<= nat (Reduce-Same)
nat =<= nat (Reduce-Same)
nat =<= nat (Reduce-Same)
nat =<= nat (Reduce-Same) OK
(nat -> nat) =<= nat (App-FO)
_0 =?= 0 (Reduce-Same) ERR
(nat -> nat) =<= nat (App-FO)
nat =<= nat (Reduce-Same)
nat =<= nat (Reduce-Same)
nat =<= nat (Reduce-Same) ERR
(?x = ?x) =<= (match 0 with
 | 0 => (?n : nat -> nat) 0
 | S _ => 1
 end = 1) (App-FO) OK
_@eq =<= @eq (Rigid-Same) OK
_?A =?= nat (Meta-Inst) OK
__Set =<= Type (Reduce-Same) OK
_?x =?= match 0 with
| 0 => (?n : nat -> nat) 0
| S _ => 1
end (Meta-Inst) OK
__nat =<= nat (Reduce-Same) OK
_match 0 with
| 0 => (?n : nat -> nat) 0
| S _ => 1
end =?= 1 (Case-IotaL) OK
__(?n 0) =?= 1 (Meta-FO) OK
___?n =?= S (Meta-Inst) OK
____(nat -> nat) =<= (nat -> nat) (Reduce-Same) OK
___0 =?= 0 (Reduce-Same)
nat =<= nat (Reduce-Same)
inst1 = eq_refl
     : (fun _ : nat => 0) x = 0
?T =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
?T@\{x:=x; x0:=x\} =<= ?A (Meta-Inst)
_?A =<= ?T@\{x:=x; x0:=x\} (Meta-Inst)
?T@\{x:=x; x0:=x\} =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
?A =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same) OK
?A =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same)
(x = x) =<= (?n x = x) (App-FO)
_@eq =<= @eq (Rigid-Same)
_nat =?= nat (Reduce-Same)
_(?n x) =?= x (Meta-Inst)
_(?n x) =?= x (Meta-DelDeps)
__(?n x) =?= x (Meta-Inst)
___(nat -> nat) =<= (nat -> nat) (Reduce-Same)
_x =?= x (Reduce-Same)
inst2 = eq_refl
     : (fun n : nat => n) x = x
 OK
(?x = ?x) =<= ((?n : nat -> nat) 0 = 0) (App-FO) ERR
_@eq =<= @eq (Rigid-Same) OK
_?A =?= nat (Meta-Inst) OK
__Set =<= Type (Reduce-Same) OK
_?x =?= (?n 0) (Meta-Inst) OK
__nat =<= nat (Reduce-Same)?T =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
?T@\{x:=x; x0:=x\} =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same) OK
(?x = ?x) =<= ((?n : nat -> nat) 0 = 0) (App-FO) ERR
_@eq =<= @eq (Rigid-Same) OK
_?A =?= nat (Meta-Inst) OK
__Set =<= Type (Reduce-Same) OK
_?x =?= (?n 0) (Meta-Inst) OK
__nat =<= nat (Reduce-Same)
?T@\{x:=x; y:=y; x0:=x; x1:=y\} =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
?T@\{x:=x; y:=y; z:=z; x0:=x; x1:=y; x2:=z\} =<= ?A (Meta-Inst)
_?A =<= ?T@\{x:=x; y:=y; z:=z; x0:=x; x1:=y; x2:=z\} (Meta-Inst)
?T@\{x:=x; y:=y; z:=z; x0:=x; x1:=y; x2:=z\} =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
?A =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
(x = x) =<= (?n x y z = x) (App-FO)
_@eq =<= @eq (Rigid-Same)
_nat =?= nat (Reduce-Same)
_(?n x y z) =?= x (Meta-Inst)
_(?n x y z) =?= x (Meta-DelDeps)
__(?n x y z) =?= x (Meta-Inst)
___(nat -> nat -> nat -> nat) =<= (nat -> nat -> nat -> nat) (Reduce-Same)
_x =?= x (Reduce-Same)
inst3 = eq_refl
     : (fun n _ _ : nat => n) x y z = x
?T =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
?T@\{x:=x; x0:=x\} =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
?T@\{x:=x; y:=y; x0:=x; x1:=y\} =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
?T@\{x:=x; y:=y; z:=z; x0:=x; x1:=y; x2:=z\} =<= ?A (Meta-Inst)
_?A =<= ?T@\{x:=x; y:=y; z:=z; x0:=x; x1:=y; x2:=z\} (Meta-Inst)
?T@\{x:=x; y:=y; z:=z; x0:=x; x1:=y; x2:=z\} =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
?A =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
(z = z) =<= (?n x y z = z) (App-FO)
_@eq =<= @eq (Rigid-Same)
_nat =?= nat (Reduce-Same)
_(?n x y z) =?= z (Meta-Inst)
_(?n x y z) =?= z (Meta-DelDeps)
__(?n x y z) =?= z (Meta-Inst)
___(nat -> nat -> nat -> nat) =<= (nat -> nat -> nat -> nat) (Reduce-Same)
_z =?= z (Reduce-Same)
inst4 = eq_refl
     : (fun _ _ n1 : nat => n1) x y z = z
 OK
?A =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same)Decimal.uint =<= Decimal.uint (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Number.uint =<= Number.uint (Reduce-Same)
nat =<= nat (Reduce-Same)
?A =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
nat =<= nat (Reduce-Same)
(@eq ?A ?x ?x) =<= (let X : forall _ : nat, nat := ?n in @eq nat (X x) O) (Let-ZetaR)
_(@eq ?A ?x ?x) =<= (@eq nat (?n x) O) (App-FO)
__@eq =<= @eq (Rigid-Same)
__?A =?= nat (Meta-Inst)
___Set =<= Type (Reduce-Same)
__(?n x) =?= ?x (Meta-Inst)
__?x =?= (?n x) (Meta-Inst)
___nat =<= nat (Reduce-Same)
__(?n x) =?= O (Meta-Inst)
___(forall _ : nat, nat) =<= (forall _ : nat, nat) (Reduce-Same) OK
(?x = ?x) =<= ((?n : nat -> nat) 0 = 0) (App-FO) OK
_@eq =<= @eq (Rigid-Same) OK
_?A =?= nat (Meta-Inst) OK
__Set =<= Type (Reduce-Same) OK
_?x =?= (?n 0) (Meta-Inst) OK
__nat =<= nat (Reduce-Same) OK
_((fun x : nat => ?n) 0) =?= 0 (Meta-Specialize) OK
__?n =?= 0 (Meta-DelDeps) OK
___?n =?= 0 (Meta-Inst) OK
____nat =<= nat (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Number.uint =<= Number.uint (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Number.uint =<= Number.uint (Reduce-Same)
?A =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
nat =<= nat (Reduce-Same)
nat =<= nat (Reduce-Same)
?A =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
(@eq nat (let X : forall _ : nat, nat := ?n in X x)
   (let X : forall _ : nat, nat := ?n in X x)) =<= (@eq nat O O) (App-FO)
_@eq =<= @eq (Rigid-Same)
_nat =?= nat (Reduce-Same) OK
?A =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same)
_(let X : forall _ : nat, nat := ?n in X x) =?= O (App-FO)
_(let X : forall _ : nat, nat := ?n in X x) =?= O (Let-ZetaL)
__(?n x) =?= O (Meta-Inst)
___(forall _ : nat, nat) =<= (forall _ : nat, nat) (Reduce-Same)
_(let X : forall _ : nat, nat := fun _ : nat => O in X x) =?= O (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Number.uint =<= Number.uint (Reduce-Same)
?T =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
?T@\{x:=x; x0:=x\} =<= ?A (Meta-Inst)
_?A =<= ?T@\{x:=x; x0:=x\} (Meta-Inst)
?T@\{x:=x; x0:=x\} =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same) OK
(?x = ?x) =<= ((?n : nat -> nat) 0 = 0) (App-FO) OK
_@eq =<= @eq (Rigid-Same) OK
_?A =?= nat (Meta-Inst) OK
__Set =<= Type (Reduce-Same) OK
_?x =?= (?n 0) (Meta-Inst) OK
__nat =<= nat (Reduce-Same) OK
_((fun x : nat => ?n) 0) =?= 0 (Meta-Specialize) OK
__?n =?= 0 (Meta-DelDeps) OK
___?n =?= 0 (Meta-Inst) OK
____nat =<= nat (Reduce-Same)
(@eq ?A ?x ?x) =<= (@eq nat ((fun w : forall _ : nat, nat => w) ?w x) O) (App-FO)
_@eq =<= @eq (Rigid-Same)
_?A =?= nat (Meta-Inst)
__Set =<= Type (Reduce-Same)
_?x =?= ((fun w : forall _ : nat, nat => w) ?w x) (Meta-Inst)
__nat =<= nat (Reduce-Same)
_(?w x) =?= O (Meta-Inst)
__(forall _ : nat, nat) =<= (forall _ : nat, nat) (Reduce-Same) OK
?T =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same) OK
?T@\{x:=x; x0:=x\} =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Number.uint =<= Number.uint (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same) OK
?T@\{x:=x; x0:=x; x1:=x\} =<= ?A (Meta-Inst) ERR
_?A =<= ?T@\{x:=x; x0:=x; x1:=x\} (Meta-Inst)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Number.uint =<= Number.uint (Reduce-Same)
?A =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same) OK
?T@\{x:=x; x0:=x; x1:=x\} =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same)
nat =<= nat (Reduce-Same)
?T =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
?T@\{x:=x; x0:=x\} =<= ?A (Meta-Inst)
_?A =<= ?T@\{x:=x; x0:=x\} (Meta-Inst)
(@eq ?T@\{x:=x; x0:=x\} ((fun w : forall x0 : nat, ?T => w) ?w x)
   ((fun w : forall x0 : nat, ?T => w) ?w x)) =<= (@eq nat O O) (App-FO)
_@eq =<= @eq (Rigid-Same)
_?T@\{x:=x; x0:=x\} =?= nat (Meta-Inst)
__Set =<= Type (Reduce-Same)
_((fun w : forall _ : nat, nat => w) ?w x) =?= O (Lam-BetaL) OK
(?x = ?x) =<= (?n x x = S x) (App-FO)
__(?w x) =?= O (Meta-Inst) ERR
_@eq =<= @eq (Rigid-Same) OK
_?A =?= nat (Meta-Inst) OK
__Set =<= Type (Reduce-Same) OK
_(?n x x) =?= ?x (Meta-Inst) ERR
_?x =?= (?n x x) (Meta-Inst) OK
__nat =<= nat (Reduce-Same) OK
_(?n x x) =?= (S x) (Meta-Inst) ERR
_(?n x x) =?= (S x) (Meta-DelDeps) ERR
__(?n x x) =?= (S x) (Meta-Inst)
___(forall _ : nat, nat) =<= (forall _ : nat, nat) (Reduce-Same)
_((fun w : forall _ : nat, nat => w) (fun _ : nat => O) x) =?= O (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Number.uint =<= Number.uint (Reduce-Same) ERR
(?x = ?x) =<= (?n x x = S x) (App-FO) ERR
_@eq =<= @eq (Rigid-Same) OK
_?A =?= nat (Meta-Inst) OK
__Set =<= Type (Reduce-Same) OK
_(?n x x) =?= ?x (Meta-Inst) ERR
_?x =?= (?n x x) (Meta-Inst) OK
__nat =<= nat (Reduce-Same) OK
_(?n x x) =?= (S x) (Meta-Inst) ERR
_(?n x x) =?= (S x) (Meta-DelDeps) ERR
__(?n x x) =?= (S x) (Meta-Inst)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Number.uint =<= Number.uint (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Number.uint =<= Number.uint (Reduce-Same)
Type =<= Type (Reduce-Same)
?T =<= nat (Meta-DelDeps)
_?T =<= nat (Meta-Inst)
__Set =<= Type (Reduce-Same)
nat =<= nat (Reduce-Same)
nat =<= nat (Reduce-Same)
(@eq ?A ?x ?x) =<= (@eq nat match O return nat with
         | O => ?n
         | S _ => O
         end x) (App-FO)
_@eq =<= @eq (Rigid-Same)
_?A =?= nat (Meta-Inst)
__Set =<= Type (Reduce-Same)
_?x =?= match O return nat with
| O => ?n
| S _ => O
end (Meta-Inst)
__nat =<= nat (Reduce-Same)
_match O return nat with
| O => ?n
| S _ => O
end =?= x (App-FO)
_match O return nat with
| O => ?n
| S _ => O
end =?= x (Case-IotaL)
__?n =?= x (Meta-Inst)
___nat =<= nat (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Number.uint =<= Number.uint (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Number.uint =<= Number.uint (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Number.uint =<= Number.uint (Reduce-Same)
Type =<= Type (Reduce-Same)
?T0 =<= (forall _ : ?T@\{n:=_ANONYMOUS_REL_1\}, nat) (Meta-DelDeps)
_?T0 =<= (forall _ : ?T@\{n:=_ANONYMOUS_REL_1\}, nat) (Meta-Inst)
__Type =<= Type (Reduce-Same)
?T =<= nat (Meta-Inst) ERR
0 =?= 0 (App-FO)
_Set =<= Type (Reduce-Same) OK
_0 =?= 0 (Rigid-Same)
?A =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
nat =<= nat (Reduce-Same)
(@eq ?A ?x ?x) =<= (@eq nat
   (match O return (forall _ : nat, nat) with
    | O => ?n
    | S _ => fun _ : nat => O
    end x) x) (App-FO)
_@eq =<= @eq (Rigid-Same)
_?A =?= nat (Meta-Inst)
__Set =<= Type (Reduce-Same)
_?x =?= (match O return (forall _ : nat, nat) with
 | O => ?n
 | S _ => fun _ : nat => O
 end x) (Meta-Inst)
__nat =<= nat (Reduce-Same)
_(match O return (forall _ : nat, nat) with
 | O => ?n
 | S _ => fun _ : nat => O
 end x) =?= x (Case-IotaL)
__(?n x) =?= x (Meta-Inst)
__(?n x) =?= x (Meta-DelDeps)
___(?n x) =?= x (Meta-Inst)
____(forall _ : nat, nat) =<= (forall _ : nat, nat) (Reduce-Same)
?A =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
nat =<= nat (Reduce-Same) OK
Decimal.uint <?= Decimal.uint

Decimal.uint =<= Decimal.uint (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Number.uint =<= Number.uint (Reduce-Same)Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint

Decimal.uint =<= Decimal.uint (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Number.uint =<= Number.uint (Reduce-Same)Decimal.uint <?= Decimal.uint

Decimal.uint =<= Decimal.uint (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)Decimal.uint <?= Decimal.uint

Number.uint =<= Number.uint (Reduce-Same)
Type =<= Type (Reduce-Same)
?T0 =<= (forall _ : ?T@\{n:=_ANONYMOUS_REL_1\}, nat) (Meta-DelDeps)
_?T0 =<= (forall _ : ?T@\{n:=_ANONYMOUS_REL_1\}, nat) (Meta-Inst)
__Type =<= Type (Reduce-Same)
?T =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
?A =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)tt
     : unit

(@eq nat
   (match O return (forall _ : nat, nat) with
    | O => ?n
    | S _ => fun _ : nat => O
    end x)
   (match O return (forall _ : nat, nat) with
    | O => ?n
    | S _ => fun _ : nat => O
    end x)) =<= (@eq nat x x) (App-FO)
_@eq =<= @eq (Rigid-Same)
_nat =?= nat (Reduce-Same)
_(match O return (forall _ : nat, nat) with
 | O => ?n
 | S _ => fun _ : nat => O
 end x) =?= x (Case-IotaL)
__(?n x) =?= x (Meta-Inst)
__(?n x) =?= x (Meta-DelDeps)
___(?n x) =?= x (Meta-Inst)
____(forall _ : nat, nat) =<= (forall _ : nat, nat) (Reduce-Same)
_(match O return (forall _ : nat, nat) with
 | O => fun n : nat => n
 | S _ => fun _ : nat => O
 end x) =?= x (Reduce-Same)
nat =<= nat (Reduce-Same)
?A0 =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
nat =<= nat (Reduce-Same)
?B =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
?A =<= (prod nat nat) (Meta-Inst)
_Set =<= Type (Reduce-Same)
nat =<= nat (Reduce-Same)
?A =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
?B =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
(prod nat nat) =<= (prod nat nat) (Reduce-Same)
(@eq ?A ?x ?x) =<= (let X : forall _ : nat, nat := ?n in
 @eq (prod nat nat) (@pair nat nat (X x) (X x)) (@pair nat nat (X x) x)) (Let-ZetaR)
_(@eq ?A ?x ?x) =<= (@eq (prod nat nat) (@pair nat nat (?n x) (?n x)) (@pair nat nat (?n x) x)) (App-FO)
__@eq =<= @eq (Rigid-Same)
__?A =?= (prod nat nat) (Meta-Inst)
___Set =<= Type (Reduce-Same)
__?x =?= (@pair nat nat (?n x) (?n x)) (Meta-Inst)
___(prod nat nat) =<= (prod nat nat) (Reduce-Same)
__(@pair nat nat (?n x) (?n x)) =?= (@pair nat nat (?n x) x) (App-FO)
___@pair =?= @pair (Rigid-Same)
___nat =?= nat (Reduce-Same)
___nat =?= nat (Reduce-Same)
___(?n x) =?= (?n x) (Meta-Same-Same)
____x =?= x (Reduce-Same)
___(?n x) =?= x (Meta-Inst)
___(?n x) =?= x (Meta-DelDeps)
____(?n x) =?= x (Meta-Inst)
_____(forall _ : nat, nat) =<= (forall _ : nat, nat) (Reduce-Same)
?A0 =<= T (Meta-Inst)
_Type =<= Type (Reduce-Same)
T =<= T (Reduce-Same)
?A =<= Prop (Meta-Inst)
_Type =<= Type (Reduce-Same)
Prop =<= Prop (Reduce-Same)
(@eq ?A0 ?x0 ?x0) =<= (@eq Prop (forall (T : Type) (t : T), @eq T t t)
   (forall (T : ?T) (t : ?T0), @eq ?A ?x ?y)) (App-FO)
_@eq =<= @eq (Rigid-Same)
_?A0 =?= Prop (Meta-Inst)
__Type =<= Type (Reduce-Same)
_?x0 =?= (forall (T : Type) (t : T), @eq T t t) (Meta-Inst)
__Prop =<= Prop (Reduce-Same)
_(forall (T : Type) (t : T), @eq T t t) =?= (forall (T : ?T) (t : ?T0), @eq ?A ?x ?y) (App-FO)
__(forall (T : Type) (t : T), @eq T t t) =?= (forall (T : ?T) (t : ?T0), @eq ?A ?x ?y) (Prod-Same)
___?T =?= Type (Meta-Inst)
____Type =<= Type (Reduce-Same)COQC test-suite/bug_44.v

___(forall t : T, @eq T t t) =?= (forall t : ?T, @eq ?A ?x ?y) (App-FO)
____(forall t : T, @eq T t t) =?= (forall t : ?T, @eq ?A ?x ?y) (Prod-Same)
_____?T =?= T (Meta-Inst)
______Type =<= Type (Reduce-Same)
_____(@eq T t t) =?= (@eq ?A ?x ?y) (App-FO)
______@eq =?= @eq (Rigid-Same)
______?A =?= T (Meta-Inst)
_______Type =<= Type (Reduce-Same)
______?x =?= t (Meta-Inst)(let x := True in ?Goal)

_______T =<= T (Reduce-Same)
______?t =?= t (Meta-Inst)
_______T =<= T (Reduce-Same)
prod1 = 
@eq_refl Prop (forall (T : Type) (t : T), @eq T t t)
     : @eq Prop (forall (T : Type) (t : T), @eq T t t)
         (forall (T : Type) (t : T), @eq T t t)
?A =<= Prop (Meta-Inst)
_Type =<= Type (Reduce-Same)
Prop =<= Prop (Reduce-Same)
(@eq ?A ?x ?x) =<= (@eq Prop (forall _ : Prop, True) (forall t : Prop, ?P : Prop)) (App-FO)
_@eq =<= @eq (Rigid-Same)
_?A =?= Prop (Meta-Inst)
__Type =<= Type (Reduce-Same)
_?x =?= (forall _ : Prop, True) (Meta-Inst)
__Prop =<= Prop (Reduce-Same)
_(forall _ : Prop, True) =?= (forall t : Prop, ?P : Prop) (App-FO)
__(forall _ : Prop, True) =?= (forall t : Prop, ?P : Prop) (Prod-Same)
___Prop =?= Prop (Reduce-Same)
___?P =?= True (Meta-Inst)
____Prop =<= Prop (Reduce-Same)
Number.uint <?= Number.uint
nat <?= nat
nat <?= nat
0 <?= X
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
0 <?= ?X
nat <?= nat
nat <?= nat
nat <?= nat
0 =<= X (App-FO) ERR
_0 =<= X (Cons-DeltaNotStuckR) OK
__?X =<= 0 (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
nat <?= nat
nat <?= nat
X =?= 0
nat <?= nat
nat <?= nat
X =?= 0 (App-FO) ERR
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
nat <?= nat
nat <?= nat
0 =?= X
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
0 =?= 0
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
0 =?= X (App-FO) ERR
_0 =?= X (Cons-DeltaNotStuckR) OK
__0 =?= 0 (App-FO) OK
___0 =?= 0 (Rigid-Same) OK
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
(S ?n) =?= (1 + 0)
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
(S ?n) =?= (S
   ((fix add (n m : nat) {struct n} : nat :=
       match n with
       | 0 => m
       | S p => S (add p m)
       end) 0 0))
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
(nat -> nat) <?= nat
(nat -> nat) =<= nat (App-FO) ERR
(nat -> nat) <?= nat
(nat -> nat) =<= nat (App-FO) ERR
(nat -> nat) <?= nat
(nat -> nat) =<= nat (App-FO) ERR
(nat -> nat) <?= nat
(nat -> nat) =<= nat (App-FO) ERR
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
?n =?= ((fix add (n m : nat) {struct n} : nat :=
    match n with
    | 0 => m
    | S p => S (add p m)
    end) 0 0)
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
(S ?n) =?= (1 + 0) (Cons-DeltaNotStuckR) OK
_(S ?n) =?= (S
   ((fix add (n m : nat) \{struct n\} : nat :=
       match n with
       | 0 => m
       | S p => S (add p m)
       end) 0 0)) (App-FO) OK
__S =?= S (Rigid-Same) OK
__?n =?= ((fix add (n m : nat) \{struct n\} : nat :=
    match n with
    | 0 => m
    | S p => S (add p m)
    end) 0 0) (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
nat <?= nat
nat <?= nat
nat <?= ?T
Set <?= Type
?T =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
(S ?n) =?= (0 + (fun x : nat => x) 1)
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
(S ?n) =?= 1
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
(nat -> nat) <?= nat
(nat -> nat) =<= nat (App-FO) ERR
(nat -> nat) <?= nat
(nat -> nat) =<= nat (App-FO) ERR
(nat -> nat) <?= nat
(nat -> nat) =<= nat (App-FO) ERR
(nat -> nat) <?= nat
(nat -> nat) =<= nat (App-FO) ERR
nat <?= nat
nat <?= nat
?n =?= 0
nat <?= nat
nat <?= nat
nat <?= nat
(S ?n) =?= (0 + (fun x : nat => x) 1) (Cons-DeltaNotStuckR) OK
_(S ?n) =?= 1 (App-FO) OK
__S =?= S (Rigid-Same) OK
__?n =?= 0 (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
nat <?= nat
nat <?= nat
nat <?= ?T
Set <?= Type
?T =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
(0 + (fun x : nat => x) 1) =?= 1
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
nat <?= nat
nat <?= nat
?y =?= 0
nat <?= nat
nat <?= nat
nat <?= ?T
Set <?= Type
?y =?= 0 (Meta-Inst) OK
_?T =<= nat (Meta-Inst) OK
__Set =<= Type (Reduce-Same) OK
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
nat <?= ?T
Set <?= Type
?T =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
nat <?= nat
nat <?= nat
(?y X) =?= 0
nat <?= nat
nat <?= nat
(nat -> nat) <?= (forall x0 : nat, ?T)
nat =?= nat
nat <?= ?T@{x0:=n}
Set <?= Type
(?y X) =?= 0 (Meta-Inst) OK
_(nat -> nat) =<= (forall x0 : nat, ?T) (App-FO) OK
__(nat -> nat) =<= (forall x0 : nat, ?T) (Prod-Same) OK
___nat =?= nat (Reduce-Same) OK
___?T@\{x0:=n\} =<= nat (Meta-Inst) OK
____Set =<= Type (Reduce-Same) OK
nat <?= ?T
Set <?= Type
?T =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
nat <?= ?T@{X:=X; x0:=X}
Set <?= Type
?T@\{X:=X; x0:=X\} =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
(?y X X) =?= X
(?y X X) =?= X
nat <?= nat
nat <?= nat
(?y X X) =?= 0
nat <?= nat
nat <?= nat
(nat -> nat -> nat) <?= (forall x0 x1 : nat, ?T)
nat =?= nat
(nat -> nat) <?= (forall x1 : nat, ?T@{x0:=n})
nat =?= nat
nat <?= ?T@{x0:=n; x1:=n}
Set <?= Type
(?y X X) =?= X (Meta-Inst) ERR
_(?y X X) =?= X (Meta-DelDeps) ERR
_(?y X X) =?= X (Meta-Reduce) OK
__(?y X X) =?= 0 (Meta-Inst) OK
___(nat -> nat -> nat) =<= (forall x0 x1 : nat, ?T) (App-FO) OK
____(nat -> nat -> nat) =<= (forall x0 x1 : nat, ?T) (Prod-Same) OK
_____nat =?= nat (Reduce-Same) OK
_____(nat -> nat) =<= (forall x1 : nat, ?T@\{x0:=n\}) (App-FO) OK
______(nat -> nat) =<= (forall x1 : nat, ?T@\{x0:=n\}) (Prod-Same) OK
_______nat =?= nat (Reduce-Same) OK
_______?T@\{x0:=n; x1:=n\} =<= nat (Meta-Inst) OK
________Set =<= Type (Reduce-Same) OK
nat <?= ?T
Set <?= Type
?T =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
nat <?= ?T@{x:=x; x0:=x}
Set <?= Type
?T@\{x:=x; x0:=x\} =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
(?y x x) =?= ?y0
(?y0 x x) =?= ?y
(?y x x) =?= ?y0 (Meta-Inst) ERR
_(?y0 x x) =?= ?y (Meta-DelDeps) ERR
nat <?= ?T
Set <?= Type
?T =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
nat <?= ?T@{x:=x; x0:=x}
Set <?= Type
?T@\{x:=x; x0:=x\} =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
(?y x x) <?= ?y0
?T@{x:=x; x0:=x; x1:=x} <?= ?T0
?y0 =<= (?y x x) (Meta-Inst) OK
_?T@\{x:=x; x0:=x; x1:=x\} =<= ?T0 (Meta-Inst) ERR
_?T0 =<= ?T@\{x:=x; x0:=x; x1:=x\} (Meta-Inst) OK
True <?= True
nat <?= ?T
Set <?= Type
?T@{x:=x; y:=x} <?= ?A
nat <?= ?T@{x:=x; y:=x}
Set <?= Type
(?x = ?x) <?= ((fun y : nat => ?n) x = x)
?A =?= nat
Set <?= Type
?x =?= ((fun y : nat => ?n) x)
nat <?= nat
?n@{x:=x; y:=x} =?= x
?n@{y:=x} =?= x
nat <?= nat
aggressive_double_var = 
fun x : nat => eq_refl
     : forall x : nat, (fun y : nat => y) x = x

Arguments aggressive_double_var x%nat_scope
nat <?= ?T
Set <?= Type
nat <?= ?T@{x:=x; z:=x}
Set <?= Type
?T@{x:=x; y:=y; z:=x; x0:=y} <?= ?A
nat <?= nat
nat <?= nat
nat <?= ?T@{x:=x; y:=y; z:=x; x0:=y}
Set <?= Type
(?x = ?x) <?= ((fun z : nat => ?n) x y = x + y)
?A =?= nat
Set <?= Type
?x =?= ((fun z : nat => ?n) x y)
nat <?= nat
(?n@{x:=x; z:=x} y) =?= (x + y)
?n@{x:=x; z:=x} =?= (Nat.add x)
?n@{z:=x} =?= (Nat.add x)
(nat -> nat) <?= (nat -> nat)
y =?= y
aggressive_double_var' = 
fun x y : nat => eq_refl
     : forall x y : nat, (fun z : nat => Nat.add z) x y = x + y

Arguments aggressive_double_var' (x y)%nat_scope
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
nat <?= ?T
Set <?= Type
nat <?= ?T@{x:=x; u:=x}
Set <?= Type
nat <?= nat
nat <?= nat
nat <?= ?T@{x:=x; u:=x; v:=0}
nat <?= ?T0@{u:=x}
Set <?= Type
nat <?= nat
nat <?= nat
?T@{x:=x; y:=y; u:=x; v:=0; w:=y} <?= ?A
nat <?= nat
nat <?= nat
nat <?= ?T@{x:=x; y:=y; u:=x; v:=0; w:=y}
nat <?= ?T@{u:=x; w:=y}
Set <?= Type
nat <?= nat
nat <?= nat
(?x = ?x) <?= ((fun u v w : nat => ?n) x 0 y = x)
?A =?= nat
Set <?= Type
nat <?= nat
nat <?= nat
?x =?= ((fun u v w : nat => ?n) x 0 y)
nat <?= nat
nat <?= nat
nat <?= nat
?n@{x:=x; y:=y; u:=x; v:=0; w:=y} =?= x
?n@{u:=x; w:=y} =?= x
nat <?= nat
nat <?= nat
nat <?= nat
aggressive_const = 
fun x _ _ : nat => eq_refl
     : forall x y : nat, nat -> (fun u _ _ : nat => u) x 0 y = x

Arguments aggressive_const (x y z)%nat_scope
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
?T@{x:=x; y:=y; u:=0; v:=x; w:=y} <?= ?A
nat <?= nat
nat <?= nat
?A =<= ?T@\{x:=x; y:=y; u:=0; v:=x; w:=y\} (Meta-Inst) OK
nat <?= nat
nat <?= nat
nat <?= ?T@{x:=x; y:=y; u:=0; v:=x; w:=y}
nat <?= ?T@{v:=x; w:=y}
Set <?= Type
?T@\{v:=x; w:=y\} =<= nat (Meta-DelDeps) OK
_?T@\{v:=x; w:=y\} =<= nat (Meta-Inst) OK
__Set =<= Type (Reduce-Same) OK
nat <?= nat
nat <?= nat
(?x = ?x) <?= ((fun u v w : nat => ?n) 0 x y = x)
nat <?= nat
nat <?= nat
?A =?= nat
Set <?= Type
nat <?= nat
nat <?= nat
?x =?= ((fun u v w : nat => ?n) 0 x y)
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
?n@{x:=x; y:=y; u:=0; v:=x; w:=y} =?= x
?n@{v:=x; w:=y} =?= x
nat <?= nat
(?x = ?x) =<= ((fun u v w : nat => ?n) 0 x y = x) (App-FO) OK
_@eq =<= @eq (Rigid-Same) OK
_?A =?= nat (Meta-Inst) OK
__Set =<= Type (Reduce-Same) OK
_?x =?= ((fun u v w : nat => ?n) 0 x y) (Meta-Inst) OK
__nat =<= nat (Reduce-Same) OK
_?n@\{v:=x; w:=y\} =?= x (Meta-DelDeps) OK
__?n@\{v:=x; w:=y\} =?= x (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
nat <?= nat
nat <?= nat
aggressive_const' = 
fun x _ _ : nat => eq_refl
     : forall x y : nat, nat -> (fun _ v _ : nat => v) 0 x y = x

Arguments aggressive_const' (x y z)%nat_scope
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
nat <?= ?T
Set <?= Type
?T =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
nat <?= ?T@{y:=y; u:=y}
Set <?= Type
?T@\{y:=y; u:=y\} =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
nat <?= ?T@{x:=x; y:=y; u:=y; v:=x}
Set <?= Type
?T@\{x:=x; y:=y; u:=y; v:=x\} =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
nat <?= nat
nat <?= nat
?T@{x:=x; y:=y; u:=y; v:=x; w:=0} <?= ?A
nat <?= nat
nat <?= nat
?A =<= ?T@\{x:=x; y:=y; u:=y; v:=x; w:=0\} (Meta-Inst) OK
nat <?= nat
nat <?= nat
nat <?= ?T@{x:=x; y:=y; u:=y; v:=x; w:=0}
nat <?= ?T@{u:=y; v:=x}
Set <?= Type
?T@\{u:=y; v:=x\} =<= nat (Meta-DelDeps) OK
_?T@\{u:=y; v:=x\} =<= nat (Meta-Inst) OK
__Set =<= Type (Reduce-Same) OK
nat <?= nat
nat <?= nat
(?x = ?x) <?= ((fun u v w : nat => ?n) y x 0 = x)
nat <?= nat
nat <?= nat
?A =?= nat
Set <?= Type
nat <?= nat
nat <?= nat
?x =?= ((fun u v w : nat => ?n) y x 0)
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
?n@{x:=x; y:=y; u:=y; v:=x; w:=0} =?= x
?n@{u:=y; v:=x} =?= x
nat <?= nat
(?x = ?x) =<= ((fun u v w : nat => ?n) y x 0 = x) (App-FO) OK
_@eq =<= @eq (Rigid-Same) OK
_?A =?= nat (Meta-Inst) OK
__Set =<= Type (Reduce-Same) OK
_?x =?= ((fun u v w : nat => ?n) y x 0) (Meta-Inst) OK
__nat =<= nat (Reduce-Same) OK
_?n@\{u:=y; v:=x\} =?= x (Meta-DelDeps) OK
__?n@\{u:=y; v:=x\} =?= x (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
nat <?= nat
nat <?= nat
aggressive_const'' = 
fun x _ _ : nat => eq_refl
     : forall x y : nat, nat -> (fun _ v _ : nat => v) y x 0 = x

Arguments aggressive_const'' (x y z)%nat_scope
Type <?= Type
?T <?= Type
Type <?= Type
?T =<= Type (Meta-Inst) OK
_Type =<= Type (Reduce-Same) OK
B <?= B
B <?= B
B <?= ?A
Type <?= Type
?A =<= B (Meta-Inst) OK
_Type =<= Type (Reduce-Same) OK
B <?= B
Prop <?= Prop
(B -> Prop) <?= (B -> Prop)
(B -> B -> Prop) <?= (B -> B -> Prop)
Prop <?= Prop
((forall B : Type, (B -> B -> Prop) -> Prop) -> Prop) <?= ((forall B : Type, (B -> B -> Prop) -> Prop) -> Prop)
?T0 <?= ?A
?A =<= ?T0 (Meta-Inst) OK
?T1 <?= ?T0
?T1 =<= ?T0 (Meta-Inst) OK
?T <?= A
Type <?= Type
?T =<= A (Meta-Inst) OK
_Type =<= Type (Reduce-Same) OK
B <?= ?T
Type <?= Type
?T =<= B (Meta-Inst) OK
_Type =<= Type (Reduce-Same) OK
A <?= A
B <?= ?T@{x:=f1 x1}
B <?= ?T0
Type <?= Type
?T0 =<= B (Meta-DelDeps) OK
_?T0 =<= B (Meta-Inst) OK
__Type =<= Type (Reduce-Same) OK
?T@{x:=f1 x1; x0:=f2 x2} <?= Prop
?T <?= Prop
Type <?= Type
?T =<= Prop (Meta-DelDeps) OK
_?T =<= Prop (Meta-Inst) OK
__Type =<= Type (Reduce-Same) OK
nat <?= nat
?T <?= Type
Type <?= Type
?T =<= Type (Meta-Inst) OK
_Type =<= Type (Reduce-Same) OK
Type <?= Type
(B -> B -> Prop) <?= (B -> B -> Prop)
((A -> B) -> (A -> B) -> Prop) <?= (?B -> ?B -> Prop)
(A -> B) =?= ?B
Type <?= Type
((A -> B) -> Prop) <?= ((A -> B) -> Prop)
((A -> B) -> (A -> B) -> Prop) =<= (?B -> ?B -> Prop) (App-FO) OK
_((A -> B) -> (A -> B) -> Prop) =<= (?B -> ?B -> Prop) (Prod-Same) OK
__?B =?= (A -> B) (Meta-Inst) OK
___Type =<= Type (Reduce-Same) OK
__((A -> B) -> Prop) =<= ((A -> B) -> Prop) (Reduce-Same) OK
Prop <?= Prop
((B -> B -> Prop) -> Prop) <?= ((B -> B -> Prop) -> Prop)
(forall B : Type, (B -> B -> Prop) -> Prop) <?= (forall B : Type, (B -> B -> Prop) -> Prop)
Prop <?= Prop
((forall B : Type, (B -> B -> Prop) -> Prop) -> Prop) <?= ((forall B : Type, (B -> B -> Prop) -> Prop) -> Prop)
((forall B : Type, (B -> B -> Prop) -> Prop) -> Prop) <?= ((forall B : Type, (B -> B -> Prop) -> Prop) -> Prop)
(nat -> nat) <?= (nat -> nat)
(nat -> nat -> nat) <?= (nat -> nat -> nat)
(nat -> nat -> nat -> nat) <?= (nat -> nat -> nat -> nat)
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= ?A
Set <?= Type
?A =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
Prop <?= Prop
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= ?A
Set <?= Type
?A =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
nat <?= nat
Prop <?= Prop
nat <?= nat
nat <?= nat
nat <?= nat
(?x = ?x) <?= ?A
Prop <?= Prop
?A =<= (?x = ?x) (Meta-Inst) OK
_Prop =<= Prop (Reduce-Same) OK
(?x0 = ?x0) <?= ?B
Prop <?= Prop
?B =<= (?x0 = ?x0) (Meta-Inst) OK
_Prop =<= Prop (Reduce-Same) OK
(?x = ?x /\ ?x0 = ?x0) <?= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) y y x /\
 (fun x y z : nat => ?n) x y z = y)
(?x = ?x) =?= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) y y x)
?A =?= nat
Set <?= Type
?x =?= ((fun x y z : nat => ?n) x y z)
nat <?= nat
?n =?= ((fun x y z : nat => ?n) y y x)
?n =?= ?n@{x:=y; y:=y; z:=x}
(?x = ?x) =?= ((fun _ y _ : nat => ?n) x y z = y)
?A =?= nat
Set <?= Type
?x =?= ((fun _ y _ : nat => ?n) x y z)
nat <?= nat
?n =?= y
nat <?= nat
(?x = ?x /\\ ?x0 = ?x0) =<= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) y y x /\\
 (fun x y z : nat => ?n) x y z = y) (App-FO) OK
_and =<= and (Rigid-Same) OK
_(?x = ?x) =?= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) y y x) (App-FO) OK
__@eq =?= @eq (Rigid-Same) OK
__?A =?= nat (Meta-Inst) OK
___Set =<= Type (Reduce-Same) OK
__?x =?= ((fun x y z : nat => ?n) x y z) (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
__?n =?= ((fun x y z : nat => ?n) y y x) (Meta-Inst) ERR
__?n =?= ((fun x y z : nat => ?n) y y x) (Meta-Reduce) OK
___?n =?= ?n (Meta-Same) OK
_(?x = ?x) =?= ((fun _ y _ : nat => ?n) x y z = y) (App-FO) OK
__@eq =?= @eq (Rigid-Same) OK
__?A =?= nat (Meta-Inst) OK
___Set =<= Type (Reduce-Same) OK
__?x =?= ((fun _ y _ : nat => ?n) x y z) (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
__?n =?= y (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
(forall z : nat,
 (fun _ y _ : nat => y) x y z = (fun _ y _ : nat => y) y y x /\
 (fun _ y _ : nat => y) x y z = y) <?= (forall z : nat,
 (fun _ y _ : nat => y) x y z = (fun _ y _ : nat => y) y y x /\
 (fun _ y _ : nat => y) x y z = y)
(forall y z : nat,
 (fun _ y0 _ : nat => y0) x y z = (fun _ y0 _ : nat => y0) y y x /\
 (fun _ y0 _ : nat => y0) x y z = y) <?= (forall y z : nat,
 (fun _ y0 _ : nat => y0) x y z = (fun _ y0 _ : nat => y0) y y x /\
 (fun _ y0 _ : nat => y0) x y z = y)
(forall x y z : nat,
 (fun _ y0 _ : nat => y0) x y z = (fun _ y0 _ : nat => y0) y y x /\
 (fun _ y0 _ : nat => y0) x y z = y) <?= (let T := fun _ y _ : nat => y in
 forall x y z : nat, T x y z = T y y x /\ T x y z = y)
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
(nat -> nat) <?= (nat -> nat)
(nat -> nat -> nat) <?= (nat -> nat -> nat)
(nat -> nat -> nat -> nat) <?= (nat -> nat -> nat -> nat)
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= ?A
Set <?= Type
?A =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
Prop <?= Prop
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= ?A
Set <?= Type
?A =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
nat <?= nat
Prop <?= Prop
nat <?= nat
nat <?= nat
nat <?= nat
(?x = ?x) <?= ?A
Prop <?= Prop
?A =<= (?x = ?x) (Meta-Inst) OK
_Prop =<= Prop (Reduce-Same) OK
(?x0 = ?x0) <?= ?B
Prop <?= Prop
?B =<= (?x0 = ?x0) (Meta-Inst) OK
_Prop =<= Prop (Reduce-Same) OK
nat <?= nat
nat <?= nat
(?x = ?x /\ ?x0 = ?x0) <?= ((fun x y z : nat => ?n) x x x = (fun x y z : nat => ?n) y y y /\
 (fun x y z : nat => ?n) x y z = 0)
nat <?= nat
nat <?= nat
(?x = ?x) =?= ((fun x y z : nat => ?n) x x x = (fun x y z : nat => ?n) y y y)
?A =?= nat
Set <?= Type
?x =?= ((fun x y z : nat => ?n) x x x)
nat <?= nat
?n@{x:=x; y:=x; z:=x} =?= ((fun x y z : nat => ?n) y y y)
?n@{z:=x} =?= ((fun _ _ z : nat => ?n) y y y)
?n@{z:=x} =?= ?n@{z:=y}
nat <?= nat
nat <?= nat
(?x = ?x) =?= ((fun _ _ _ : nat => ?n) x y z = 0)
nat <?= nat
nat <?= nat
?A =?= nat
Set <?= Type
?x =?= ((fun _ _ _ : nat => ?n) x y z)
nat <?= nat
nat <?= nat
nat <?= nat
?n =?= 0
nat <?= nat
nat <?= nat
nat <?= nat
(?x = ?x /\\ ?x0 = ?x0) =<= ((fun x y z : nat => ?n) x x x = (fun x y z : nat => ?n) y y y /\\
 (fun x y z : nat => ?n) x y z = 0) (App-FO) OK
_and =<= and (Rigid-Same) OK
_(?x = ?x) =?= ((fun x y z : nat => ?n) x x x = (fun x y z : nat => ?n) y y y) (App-FO) OK
__@eq =?= @eq (Rigid-Same) OK
__?A =?= nat (Meta-Inst) OK
___Set =<= Type (Reduce-Same) OK
__?x =?= ((fun x y z : nat => ?n) x x x) (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
__?n@\{x:=x; y:=x; z:=x\} =?= ((fun x y z : nat => ?n) y y y) (Meta-Inst) ERR
__?n@\{z:=x\} =?= ((fun _ _ z : nat => ?n) y y y) (Meta-DelDeps) OK
___?n@\{z:=x\} =?= ((fun _ _ z : nat => ?n) y y y) (Meta-Inst) ERR
___?n@\{z:=x\} =?= ((fun _ _ z : nat => ?n) y y y) (Meta-Reduce) OK
____?n =?= ?n (Meta-Same) OK
_(?x = ?x) =?= ((fun _ _ _ : nat => ?n) x y z = 0) (App-FO) OK
__@eq =?= @eq (Rigid-Same) OK
__?A =?= nat (Meta-Inst) OK
___Set =<= Type (Reduce-Same) OK
__?x =?= ((fun _ _ _ : nat => ?n) x y z) (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
__?n =?= 0 (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
(forall z : nat,
 (fun _ _ _ : nat => 0) x x x = (fun _ _ _ : nat => 0) y y y /\
 (fun _ _ _ : nat => 0) x y z = 0) <?= (forall z : nat,
 (fun _ _ _ : nat => 0) x x x = (fun _ _ _ : nat => 0) y y y /\
 (fun _ _ _ : nat => 0) x y z = 0)
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
(forall y z : nat,
 (fun _ _ _ : nat => 0) x x x = (fun _ _ _ : nat => 0) y y y /\
 (fun _ _ _ : nat => 0) x y z = 0) <?= (forall y z : nat,
 (fun _ _ _ : nat => 0) x x x = (fun _ _ _ : nat => 0) y y y /\
 (fun _ _ _ : nat => 0) x y z = 0)
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
(forall x y z : nat,
 (fun _ _ _ : nat => 0) x x x = (fun _ _ _ : nat => 0) y y y /\
 (fun _ _ _ : nat => 0) x y z = 0) <?= (let T := fun _ _ _ : nat => 0 in
 forall x y z : nat, T x x x = T y y y /\ T x y z = 0)
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
(nat -> nat) <?= (nat -> nat)
(nat -> nat -> nat) <?= (nat -> nat -> nat)
(nat -> nat -> nat -> nat) <?= (nat -> nat -> nat -> nat)
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= ?A
Set <?= Type
?A =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
Prop <?= Prop
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= ?A
Set <?= Type
?A =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
nat <?= nat
Prop <?= Prop
nat <?= nat
nat <?= nat
nat <?= nat
(?x = ?x) <?= ?A
Prop <?= Prop
?A =<= (?x = ?x) (Meta-Inst) OK
_Prop =<= Prop (Reduce-Same) OK
(?x0 = ?x0) <?= ?B
Prop <?= Prop
?B =<= (?x0 = ?x0) (Meta-Inst) OK
_Prop =<= Prop (Reduce-Same) OK
(?x = ?x /\ ?x0 = ?x0) <?= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) y y x /\
 (fun x y z : nat => ?n) x y z = x)
(?x = ?x) =?= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) y y x)
?A =?= nat
Set <?= Type
?x =?= ((fun x y z : nat => ?n) x y z)
nat <?= nat
?n =?= ((fun x y z : nat => ?n) y y x)
?n =?= ?n@{x:=y; y:=y; z:=x}
(?x = ?x) =?= ((fun _ y _ : nat => ?n) x y z = x)
?A =?= nat
Set <?= Type
?x =?= ((fun _ y _ : nat => ?n) x y z)
nat <?= nat
?n =?= x
(?x = ?x /\\ ?x0 = ?x0) =<= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) y y x /\\
 (fun x y z : nat => ?n) x y z = x) (App-FO) ERR
_and =<= and (Rigid-Same) OK
_(?x = ?x) =?= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) y y x) (App-FO) OK
__@eq =?= @eq (Rigid-Same) OK
__?A =?= nat (Meta-Inst) OK
___Set =<= Type (Reduce-Same) OK
__?x =?= ((fun x y z : nat => ?n) x y z) (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
__?n =?= ((fun x y z : nat => ?n) y y x) (Meta-Inst) ERR
__?n =?= ((fun x y z : nat => ?n) y y x) (Meta-Reduce) OK
___?n =?= ?n (Meta-Same) OK
_(?x = ?x) =?= ((fun _ y _ : nat => ?n) x y z = x) (App-FO) ERR
__@eq =?= @eq (Rigid-Same) OK
__?A =?= nat (Meta-Inst) OK
___Set =<= Type (Reduce-Same) OK
__?x =?= ((fun _ y _ : nat => ?n) x y z) (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
__?n =?= x (Meta-Inst) ERR
(?x = ?x /\ ?x0 = ?x0) <?= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) y y x /\
 (fun x y z : nat => ?n) x y z = x)
(?x = ?x) =?= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) y y x)
?A =?= nat
Set <?= Type
?x =?= ((fun x y z : nat => ?n) x y z)
nat <?= nat
?n =?= ((fun x y z : nat => ?n) y y x)
?n =?= ?n@{x:=y; y:=y; z:=x}
(?x = ?x) =?= ((fun _ y _ : nat => ?n) x y z = x)
?A =?= nat
Set <?= Type
?x =?= ((fun _ y _ : nat => ?n) x y z)
nat <?= nat
?n =?= x
(?x = ?x /\\ ?x0 = ?x0) =<= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) y y x /\\
 (fun x y z : nat => ?n) x y z = x) (App-FO) ERR
_and =<= and (Rigid-Same) OK
_(?x = ?x) =?= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) y y x) (App-FO) OK
__@eq =?= @eq (Rigid-Same) OK
__?A =?= nat (Meta-Inst) OK
___Set =<= Type (Reduce-Same) OK
__?x =?= ((fun x y z : nat => ?n) x y z) (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
__?n =?= ((fun x y z : nat => ?n) y y x) (Meta-Inst) ERR
__?n =?= ((fun x y z : nat => ?n) y y x) (Meta-Reduce) OK
___?n =?= ?n (Meta-Same) OK
_(?x = ?x) =?= ((fun _ y _ : nat => ?n) x y z = x) (App-FO) ERR
__@eq =?= @eq (Rigid-Same) OK
__?A =?= nat (Meta-Inst) OK
___Set =<= Type (Reduce-Same) OK
__?x =?= ((fun _ y _ : nat => ?n) x y z) (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
__?n =?= x (Meta-Inst) ERR
(nat -> nat) <?= (nat -> nat)
(nat -> nat -> nat) <?= (nat -> nat -> nat)
(nat -> nat -> nat -> nat) <?= (nat -> nat -> nat -> nat)
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= ?A
Set <?= Type
?A =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
Prop <?= Prop
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= ?A
Set <?= Type
?A =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
nat <?= nat
Prop <?= Prop
nat <?= nat
nat <?= nat
nat <?= nat
(?x = ?x) <?= ?A
Prop <?= Prop
?A =<= (?x = ?x) (Meta-Inst) OK
_Prop =<= Prop (Reduce-Same) OK
(?x0 = ?x0) <?= ?B
Prop <?= Prop
?B =<= (?x0 = ?x0) (Meta-Inst) OK
_Prop =<= Prop (Reduce-Same) OK
(?x = ?x /\ ?x0 = ?x0) <?= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) y y x /\
 (fun x y z : nat => ?n) x y z = x)
(?x = ?x) =?= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) y y x)
?A =?= nat
Set <?= Type
?x =?= ((fun x y z : nat => ?n) x y z)
nat <?= nat
?n =?= ((fun x y z : nat => ?n) y y x)
?n =?= ?n@{x:=y; y:=y; z:=x}
(?x = ?x) =?= ((fun _ y _ : nat => ?n) x y z = x)
?A =?= nat
Set <?= Type
?x =?= ((fun _ y _ : nat => ?n) x y z)
nat <?= nat
?n =?= x
(?x = ?x /\\ ?x0 = ?x0) =<= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) y y x /\\
 (fun x y z : nat => ?n) x y z = x) (App-FO) ERR
_and =<= and (Rigid-Same) OK
_(?x = ?x) =?= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) y y x) (App-FO) OK
__@eq =?= @eq (Rigid-Same) OK
__?A =?= nat (Meta-Inst) OK
___Set =<= Type (Reduce-Same) OK
__?x =?= ((fun x y z : nat => ?n) x y z) (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
__?n =?= ((fun x y z : nat => ?n) y y x) (Meta-Inst) ERR
__?n =?= ((fun x y z : nat => ?n) y y x) (Meta-Reduce) OK
___?n =?= ?n (Meta-Same) OK
_(?x = ?x) =?= ((fun _ y _ : nat => ?n) x y z = x) (App-FO) ERR
__@eq =?= @eq (Rigid-Same) OK
__?A =?= nat (Meta-Inst) OK
___Set =<= Type (Reduce-Same) OK
__?x =?= ((fun _ y _ : nat => ?n) x y z) (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
__?n =?= x (Meta-Inst) ERR
(?x = ?x /\ ?x0 = ?x0) <?= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) y y x /\
 (fun x y z : nat => ?n) x y z = x)
(?x = ?x) =?= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) y y x)
?A =?= nat
Set <?= Type
?x =?= ((fun x y z : nat => ?n) x y z)
nat <?= nat
?n =?= ((fun x y z : nat => ?n) y y x)
?n =?= ?n@{x:=y; y:=y; z:=x}
(?x = ?x) =?= ((fun _ y _ : nat => ?n) x y z = x)
?A =?= nat
Set <?= Type
?x =?= ((fun _ y _ : nat => ?n) x y z)
nat <?= nat
?n =?= x
(?x = ?x /\\ ?x0 = ?x0) =<= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) y y x /\\
 (fun x y z : nat => ?n) x y z = x) (App-FO) ERR
_and =<= and (Rigid-Same) OK
_(?x = ?x) =?= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) y y x) (App-FO) OK
__@eq =?= @eq (Rigid-Same) OK
__?A =?= nat (Meta-Inst) OK
___Set =<= Type (Reduce-Same) OK
__?x =?= ((fun x y z : nat => ?n) x y z) (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
__?n =?= ((fun x y z : nat => ?n) y y x) (Meta-Inst) ERR
__?n =?= ((fun x y z : nat => ?n) y y x) (Meta-Reduce) OK
___?n =?= ?n (Meta-Same) OK
_(?x = ?x) =?= ((fun _ y _ : nat => ?n) x y z = x) (App-FO) ERR
__@eq =?= @eq (Rigid-Same) OK
__?A =?= nat (Meta-Inst) OK
___Set =<= Type (Reduce-Same) OK
__?x =?= ((fun _ y _ : nat => ?n) x y z) (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
__?n =?= x (Meta-Inst) ERR
(nat -> nat) <?= (nat -> nat)
(nat -> nat -> nat) <?= (nat -> nat -> nat)
(nat -> nat -> nat -> nat) <?= (nat -> nat -> nat -> nat)
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= ?A
Set <?= Type
?A =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
Prop <?= Prop
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= ?A
Set <?= Type
?A =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
nat <?= nat
Prop <?= Prop
nat <?= nat
nat <?= nat
nat <?= nat
(?x = ?x) <?= ?A
Prop <?= Prop
?A =<= (?x = ?x) (Meta-Inst) OK
_Prop =<= Prop (Reduce-Same) OK
(?x0 = ?x0) <?= ?B
Prop <?= Prop
?B =<= (?x0 = ?x0) (Meta-Inst) OK
_Prop =<= Prop (Reduce-Same) OK
(?x = ?x /\ ?x0 = ?x0) <?= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) x z z /\
 (fun x y z : nat => ?n) x y z = x)
(?x = ?x) =?= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) x z z)
?A =?= nat
Set <?= Type
?x =?= ((fun x y z : nat => ?n) x y z)
nat <?= nat
?n =?= ((fun x y z : nat => ?n) x z z)
?n =?= ?n@{y:=z; z:=z}
(?x = ?x) =?= ((fun x _ z : nat => ?n) x y z = x)
?A =?= nat
Set <?= Type
?x =?= ((fun x _ z : nat => ?n) x y z)
nat <?= nat
?n =?= x
nat <?= nat
(?x = ?x /\\ ?x0 = ?x0) =<= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) x z z /\\
 (fun x y z : nat => ?n) x y z = x) (App-FO) OK
_and =<= and (Rigid-Same) OK
_(?x = ?x) =?= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) x z z) (App-FO) OK
__@eq =?= @eq (Rigid-Same) OK
__?A =?= nat (Meta-Inst) OK
___Set =<= Type (Reduce-Same) OK
__?x =?= ((fun x y z : nat => ?n) x y z) (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
__?n =?= ((fun x y z : nat => ?n) x z z) (Meta-Inst) ERR
__?n =?= ((fun x y z : nat => ?n) x z z) (Meta-Reduce) OK
___?n =?= ?n (Meta-Same) OK
_(?x = ?x) =?= ((fun x _ z : nat => ?n) x y z = x) (App-FO) OK
__@eq =?= @eq (Rigid-Same) OK
__?A =?= nat (Meta-Inst) OK
___Set =<= Type (Reduce-Same) OK
__?x =?= ((fun x _ z : nat => ?n) x y z) (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
__?n =?= x (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
(forall z : nat,
 (fun x _ _ : nat => x) x y z = (fun x _ _ : nat => x) x z z /\
 (fun x _ _ : nat => x) x y z = x) <?= (forall z : nat,
 (fun x _ _ : nat => x) x y z = (fun x _ _ : nat => x) x z z /\
 (fun x _ _ : nat => x) x y z = x)
(forall y z : nat,
 (fun x _ _ : nat => x) x y z = (fun x _ _ : nat => x) x z z /\
 (fun x _ _ : nat => x) x y z = x) <?= (forall y z : nat,
 (fun x _ _ : nat => x) x y z = (fun x _ _ : nat => x) x z z /\
 (fun x _ _ : nat => x) x y z = x)
(forall x y z : nat,
 (fun x0 _ _ : nat => x0) x y z = (fun x0 _ _ : nat => x0) x z z /\
 (fun x0 _ _ : nat => x0) x y z = x) <?= (let T := fun x _ _ : nat => x in
 forall x y z : nat, T x y z = T x z z /\ T x y z = x)
(nat -> nat) <?= (nat -> nat)
(nat -> nat -> nat) <?= (nat -> nat -> nat)
(nat -> nat -> nat -> nat) <?= (nat -> nat -> nat -> nat)
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= ?A
Set <?= Type
?A =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
Prop <?= Prop
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= ?A
Set <?= Type
?A =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
nat <?= nat
Prop <?= Prop
nat <?= nat
nat <?= nat
nat <?= nat
(?x = ?x) <?= ?A
Prop <?= Prop
?A =<= (?x = ?x) (Meta-Inst) OK
_Prop =<= Prop (Reduce-Same) OK
(?x0 = ?x0) <?= ?B
Prop <?= Prop
?B =<= (?x0 = ?x0) (Meta-Inst) OK
_Prop =<= Prop (Reduce-Same) OK
(?x = ?x /\ ?x0 = ?x0) <?= ((fun x y z : nat => ?n) z y z = (fun x y z : nat => ?n) z z z /\
 (fun x y z : nat => ?n) x y z = z)
(?x = ?x) =?= ((fun x y z : nat => ?n) z y z = (fun x y z : nat => ?n) z z z)
?A =?= nat
Set <?= Type
?x =?= ((fun x y z : nat => ?n) z y z)
nat <?= nat
?n@{x:=z; z:=z} =?= ((fun x y z : nat => ?n) z z z)
?n =?= ((fun _ y z : nat => ?n) z z z)
?n =?= ?n@{y:=z; z:=z}
(?x = ?x) =?= ((fun _ _ z : nat => ?n) x y z = z)
?A =?= nat
Set <?= Type
?x =?= ((fun _ _ z : nat => ?n) x y z)
nat <?= nat
?n =?= z
nat <?= nat
(?x = ?x /\\ ?x0 = ?x0) =<= ((fun x y z : nat => ?n) z y z = (fun x y z : nat => ?n) z z z /\\
 (fun x y z : nat => ?n) x y z = z) (App-FO) OK
_and =<= and (Rigid-Same) OK
_(?x = ?x) =?= ((fun x y z : nat => ?n) z y z = (fun x y z : nat => ?n) z z z) (App-FO) OK
__@eq =?= @eq (Rigid-Same) OK
__?A =?= nat (Meta-Inst) OK
___Set =<= Type (Reduce-Same) OK
__?x =?= ((fun x y z : nat => ?n) z y z) (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
__?n@\{x:=z; z:=z\} =?= ((fun x y z : nat => ?n) z z z) (Meta-Inst) ERR
__?n =?= ((fun _ y z : nat => ?n) z z z) (Meta-DelDeps) OK
___?n =?= ((fun _ y z : nat => ?n) z z z) (Meta-Inst) ERR
___?n =?= ((fun _ y z : nat => ?n) z z z) (Meta-Reduce) OK
____?n =?= ?n (Meta-Same) OK
_(?x = ?x) =?= ((fun _ _ z : nat => ?n) x y z = z) (App-FO) OK
__@eq =?= @eq (Rigid-Same) OK
__?A =?= nat (Meta-Inst) OK
___Set =<= Type (Reduce-Same) OK
__?x =?= ((fun _ _ z : nat => ?n) x y z) (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
__?n =?= z (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
(forall z : nat,
 (fun _ _ z0 : nat => z0) z y z = (fun _ _ z0 : nat => z0) z z z /\
 (fun _ _ z0 : nat => z0) x y z = z) <?= (forall z : nat,
 (fun _ _ z0 : nat => z0) z y z = (fun _ _ z0 : nat => z0) z z z /\
 (fun _ _ z0 : nat => z0) x y z = z)
(forall y z : nat,
 (fun _ _ z0 : nat => z0) z y z = (fun _ _ z0 : nat => z0) z z z /\
 (fun _ _ z0 : nat => z0) x y z = z) <?= (forall y z : nat,
 (fun _ _ z0 : nat => z0) z y z = (fun _ _ z0 : nat => z0) z z z /\
 (fun _ _ z0 : nat => z0) x y z = z)
(forall x y z : nat,
 (fun _ _ z0 : nat => z0) z y z = (fun _ _ z0 : nat => z0) z z z /\
 (fun _ _ z0 : nat => z0) x y z = z) <?= (let T := fun _ _ z : nat => z in
 forall x y z : nat, T z y z = T z z z /\ T x y z = z)
(nat -> nat) <?= (nat -> nat)
(nat -> nat -> nat) <?= (nat -> nat -> nat)
(nat -> nat -> nat -> nat) <?= (nat -> nat -> nat -> nat)
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= ?A
Set <?= Type
?A =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
Prop <?= Prop
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= ?A
Set <?= Type
?A =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
nat <?= nat
Prop <?= Prop
nat <?= nat
nat <?= nat
nat <?= nat
(?x = ?x) <?= ?A
Prop <?= Prop
?A =<= (?x = ?x) (Meta-Inst) OK
_Prop =<= Prop (Reduce-Same) OK
(?x0 = ?x0) <?= ?B
Prop <?= Prop
?B =<= (?x0 = ?x0) (Meta-Inst) OK
_Prop =<= Prop (Reduce-Same) OK
(?x = ?x /\ ?x0 = ?x0) <?= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) x z z /\
 (fun x y z : nat => ?n) x y z = y)
(?x = ?x) =?= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) x z z)
?A =?= nat
Set <?= Type
?x =?= ((fun x y z : nat => ?n) x y z)
nat <?= nat
?n =?= ((fun x y z : nat => ?n) x z z)
?n =?= ?n@{y:=z; z:=z}
(?x = ?x) =?= ((fun x _ z : nat => ?n) x y z = y)
?A =?= nat
Set <?= Type
?x =?= ((fun x _ z : nat => ?n) x y z)
nat <?= nat
?n =?= y
(?x = ?x /\\ ?x0 = ?x0) =<= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) x z z /\\
 (fun x y z : nat => ?n) x y z = y) (App-FO) ERR
_and =<= and (Rigid-Same) OK
_(?x = ?x) =?= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) x z z) (App-FO) OK
__@eq =?= @eq (Rigid-Same) OK
__?A =?= nat (Meta-Inst) OK
___Set =<= Type (Reduce-Same) OK
__?x =?= ((fun x y z : nat => ?n) x y z) (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
__?n =?= ((fun x y z : nat => ?n) x z z) (Meta-Inst) ERR
__?n =?= ((fun x y z : nat => ?n) x z z) (Meta-Reduce) OK
___?n =?= ?n (Meta-Same) OK
_(?x = ?x) =?= ((fun x _ z : nat => ?n) x y z = y) (App-FO) ERR
__@eq =?= @eq (Rigid-Same) OK
__?A =?= nat (Meta-Inst) OK
___Set =<= Type (Reduce-Same) OK
__?x =?= ((fun x _ z : nat => ?n) x y z) (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
__?n =?= y (Meta-Inst) ERR
(?x = ?x /\ ?x0 = ?x0) <?= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) x z z /\
 (fun x y z : nat => ?n) x y z = y)
(?x = ?x) =?= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) x z z)
?A =?= nat
Set <?= Type
?x =?= ((fun x y z : nat => ?n) x y z)
nat <?= nat
?n =?= ((fun x y z : nat => ?n) x z z)
?n =?= ?n@{y:=z; z:=z}
(?x = ?x) =?= ((fun x _ z : nat => ?n) x y z = y)
?A =?= nat
Set <?= Type
?x =?= ((fun x _ z : nat => ?n) x y z)
nat <?= nat
?n =?= y
(?x = ?x /\\ ?x0 = ?x0) =<= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) x z z /\\
 (fun x y z : nat => ?n) x y z = y) (App-FO) ERR
_and =<= and (Rigid-Same) OK
_(?x = ?x) =?= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) x z z) (App-FO) OK
__@eq =?= @eq (Rigid-Same) OK
__?A =?= nat (Meta-Inst) OK
___Set =<= Type (Reduce-Same) OK
__?x =?= ((fun x y z : nat => ?n) x y z) (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
__?n =?= ((fun x y z : nat => ?n) x z z) (Meta-Inst) ERR
__?n =?= ((fun x y z : nat => ?n) x z z) (Meta-Reduce) OK
___?n =?= ?n (Meta-Same) OK
_(?x = ?x) =?= ((fun x _ z : nat => ?n) x y z = y) (App-FO) ERR
__@eq =?= @eq (Rigid-Same) OK
__?A =?= nat (Meta-Inst) OK
___Set =<= Type (Reduce-Same) OK
__?x =?= ((fun x _ z : nat => ?n) x y z) (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
__?n =?= y (Meta-Inst) ERR
STATS:	902		165
Finished transaction in 22.975 secs (19.229u,0.26s) (successful)
make[1]: Leaving directory '/build/coq-unicoq-1.6-8.16'
   dh_auto_test
   create-stamp debian/debhelper-build-stamp
   dh_prep
   debian/rules override_dh_auto_install
make[1]: Entering directory '/build/coq-unicoq-1.6-8.16'
DESTDIR=debian/tmp make install
make[2]: Entering directory '/build/coq-unicoq-1.6-8.16'
INSTALL theories/Unicoq.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Unicoq/
SKIP test-suite/munifytest.vo since it has no logical path
SKIP test-suite/microtests.vo since it has no logical path
SKIP test-suite/primitive.vo since it has no logical path
SKIP test-suite/instantiate.vo since it has no logical path
SKIP test-suite/timings.vo since it has no logical path
SKIP test-suite/bug_41.vo since it has no logical path
SKIP test-suite/bug_44.vo since it has no logical path
INSTALL theories/Unicoq.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Unicoq/
SKIP test-suite/munifytest.v since it has no logical path
SKIP test-suite/microtests.v since it has no logical path
SKIP test-suite/primitive.v since it has no logical path
SKIP test-suite/instantiate.v since it has no logical path
SKIP test-suite/timings.v since it has no logical path
SKIP test-suite/bug_41.v since it has no logical path
SKIP test-suite/bug_44.v since it has no logical path
INSTALL theories/Unicoq.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Unicoq/
SKIP test-suite/munifytest.glob since it has no logical path
SKIP test-suite/microtests.glob since it has no logical path
SKIP test-suite/primitive.glob since it has no logical path
SKIP test-suite/instantiate.glob since it has no logical path
SKIP test-suite/timings.glob since it has no logical path
SKIP test-suite/bug_41.glob since it has no logical path
SKIP test-suite/bug_44.glob since it has no logical path
INSTALL src/unicoq.cmxs debian/tmp//usr/lib/ocaml/coq//user-contrib/Unicoq/
INSTALL src/unicoq.cmxs debian/tmp//usr/lib/ocaml/coq//user-contrib/Unicoq/
ocamlfind: [WARNING] No such file: debian/tmp//usr/lib/ocaml/coq/../coq-core//../coq-unicoq/META
Installed debian/tmp//usr/lib/ocaml/coq/../coq-core//../coq-unicoq/unicoq.cmx
Installed debian/tmp//usr/lib/ocaml/coq/../coq-core//../coq-unicoq/unicoq.cmxa
Installed debian/tmp//usr/lib/ocaml/coq/../coq-core//../coq-unicoq/unicoq.cmxs
ocamlfind: [WARNING] Overwriting file debian/tmp//usr/lib/ocaml/coq/../coq-core//../coq-unicoq/unicoq.cmxs
Installed debian/tmp//usr/lib/ocaml/coq/../coq-core//../coq-unicoq/unicoq.cmxs
Installed debian/tmp//usr/lib/ocaml/coq/../coq-core//../coq-unicoq/unicoq.cmi
Installed debian/tmp//usr/lib/ocaml/coq/../coq-core//../coq-unicoq/META
make[3]: Entering directory '/build/coq-unicoq-1.6-8.16'
make[3]: Leaving directory '/build/coq-unicoq-1.6-8.16'
make[2]: Leaving directory '/build/coq-unicoq-1.6-8.16'
make[1]: Leaving directory '/build/coq-unicoq-1.6-8.16'
   dh_install
   dh_ocamldoc
   dh_installdocs
   dh_installchangelogs
   dh_perl
   dh_link
   dh_strip_nondeterminism
   dh_compress
   dh_fixperms
   dh_missing
   dh_strip -a
   dh_makeshlibs -a
   dh_shlibdeps -a
   dh_installdeb
   dh_coq
   dh_ocaml
   dh_gencontrol
dpkg-gencontrol: warning: package libcoq-unicoq: substitution variable ${ocaml:Depends} unused, but is defined
dpkg-gencontrol: warning: package libcoq-unicoq: substitution variable ${ocaml:Depends} unused, but is defined
   dh_md5sums
   dh_builddeb
dpkg-deb: building package 'libcoq-unicoq-dbgsym' in '../libcoq-unicoq-dbgsym_1.6-8.16-2_armhf.deb'.
dpkg-deb: building package 'libcoq-unicoq' in '../libcoq-unicoq_1.6-8.16-2_armhf.deb'.
 dpkg-genbuildinfo --build=binary -O../coq-unicoq_1.6-8.16-2_armhf.buildinfo
 dpkg-genchanges --build=binary -O../coq-unicoq_1.6-8.16-2_armhf.changes
dpkg-genchanges: info: binary-only upload (no source code included)
 dpkg-source --after-build .
dpkg-buildpackage: info: binary-only upload (no source included)
dpkg-genchanges: info: not including original source code in upload
I: copying local configuration
I: user script /srv/workspace/pbuilder/21008/tmp/hooks/B01_cleanup starting
I: user script /srv/workspace/pbuilder/21008/tmp/hooks/B01_cleanup finished
I: unmounting dev/ptmx filesystem
I: unmounting dev/pts filesystem
I: unmounting dev/shm filesystem
I: unmounting proc filesystem
I: unmounting sys filesystem
I: cleaning the build env 
I: removing directory /srv/workspace/pbuilder/21008 and its subdirectories
I: Current time: Tue May 30 23:11:39 +14 2023
I: pbuilder-time-stamp: 1685437899