HuStmpHrrr

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

import bs4
import cgitb
import os
import sys

cgitb.enable()

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

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

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

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

Section Tests.

  Variable A : Type.

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

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