Mukesh Tiwari mukeshtiwari

The Different Types of Equality

I don't have much to say about this topic since I don't fully understand it.

Basically here are the types of equality I've found:

	From Coq Require Import
	Program.Tactics
	List Psatz.


	Program Definition nth_safe {A} (l: list A) (n: nat) (IN: (n < length l)%nat) : A :=
	match (nth_error l n) with
	\| Some res => res
	\| None => _
	end.

	(base) mukesh.tiwari@Mukeshs-MacBook-Pro-2 ~ % opam upgrade
	The following actions will be performed:
	=== recompile 9 packages
	↻ coq-elpi 2.2.3 [uses elpi, ppx_optcomp]
	↻ lsp 1.18.0 [uses ppx_yojson_conv_lib]
	↻ ocaml-lsp-server 1.18.0~5.2preview [uses base, ppx_yojson_conv_lib]
	↻ ocamlformat 0.26.2 [uses ocamlformat-lib]
	↻ ocamlformat-lib 0.26.2 [uses base, stdio]
	↻ ppx_deriving 6.0.2 [uses ppxlib]
	↻ ppx_import 1.11.0 [uses ppxlib]

	CoInductive coAcc {A : Type} (R : A -> A -> Prop) (x : A) : Prop :=
	\| coAcc_intro : (forall y : A, R x y -> coAcc R y) -> coAcc R x.


	CoFixpoint coacc_rect :
	forall (A : Type) (R : A -> A -> Prop) (P : A -> Type),
	(forall x : A, (forall y : A, R x y -> coAcc R y) ->
	(forall y : A, R x y -> P y) -> P x) -> forall x : A, coAcc R x -> P x :=
	fun (A : Type) (R : A -> A -> Prop) (P : A -> Type)
	(f : (forall x : A, (forall y : A, R x y -> coAcc R y) ->

	(* In relation to https://cstheory.stackexchange.com/questions/40631/how-can-you-build-a-coinductive-memoization-table-for-recursive-functions-over-b *)
	Require Import Vectors.Vector.
	Import VectorNotations.

	Set Primitive Projections.
	Set Implicit Arguments.

	Inductive binTree : Set :=
	\| Leaf : binTree
	\| Branch : binTree -> binTree -> binTree.

	From Coq Require Import
	Relation_Operators Utf8 Psatz Wf_nat.


	Section Morp.

	Variable A : Type.
	Variable B : Type.
	Variable leA : A -> A -> Prop. (* A relation on type A *)
	Variable leB : B -> B -> Prop. (* A relation on type B *)

	From Coq Require Import
	Relation_Operators Utf8 Psatz Wf_nat.


	Section Jason.

	Context {A B : Type}
	(f : A * B -> nat).

	Theorem fn_acc : forall (n : nat) (au : A) (bu : B),