HuStmpHrrr

open import Level
open import Data.Product

open import Categories.Category
open import Categories.NaturalTransformation as NT
open import Categories.Functor
open import Categories.Functor.Bifunctor
open import Categories.Category.Product
import Categories.Square as Square

HuStmpHrrr

From Equations Require Import Equations.
Require Import Equations.Subterm.
Require Import Lia.

Section Tests.

  Variable A : Type.

  Inductive forest : Type :=
  | emp : A -> forest

HuStmpHrrr

Set Implicit Arguments.

Require Import Coq.Lists.List.
Require Import PeanoNat.
Require Import FunInd.

Require Import Arith.Wf_nat.
Require Import Recdef.
Require Import Omega.

HuStmpHrrr

Require Import Coq.Vectors.Vector.

Definition drop {A} {m n} : Vector.t A (m + n) -> Vector.t A n.
Proof.
  induction m.
  - intros vec. exact vec.
  - intros vec. inversion vec; subst.
    apply IHm. apply X.
Defined.
                      

HuStmpHrrr

(defun coq-debug-eauto-output--transform (flag)
  (goto-char (line-beginning-position))
  (let ((line (buffer-substring-no-properties
               (line-beginning-position)
               (line-end-position))))
    (pcase line
      ("" nil)
      ("Debug: (* debug eauto: *)"
       (delete-region (line-beginning-position) (line-end-position))

HuStmpHrrr

#!/usr/bin/env python
# vim: ft=python

import bs4
import cgitb
import os
import sys

cgitb.enable()