Johannes Hostert JoJoDeveloping
JoJoDeveloping
/ Recursion.v
Last active
November 22, 2023 02:48
— forked from Agnishom/Attempt1.v
Convoy Pattern + Sigma Types + Equations
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Require Import Coq.Lists.List. | |
| Require Import Coq.Relations.Relation_Operators. | |
| Require Import Coq.Wellfounded.Lexicographic_Product. | |
| Require Import Coq.Arith.Wf_nat. | |
| Require Import Arith. | |
| Import ListNotations. | |
| Require Import Coq.Init.Nat. | |
| Require Import Lia. |