Commit 69a85681 authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

Suite d'equivalence entre alpha-equivalences :-)

parent 3a800ff9
This diff is collapsed.
......@@ -8,7 +8,7 @@
# #
###############################################################################
COQMF_VFILES = AsciiOrder.v StringOrder.v StringUtils.v Utils.v Defs.v Nam.v Alpha.v Mix.v Proofs.v Equiv.v Meta.v ToCoq.v
COQMF_VFILES = AsciiOrder.v StringOrder.v StringUtils.v Utils.v Defs.v Nam.v Alpha.v AlphaAlt.v Mix.v Proofs.v Equiv.v Meta.v ToCoq.v
COQMF_MLIFILES =
COQMF_MLFILES =
COQMF_ML4FILES =
......
......@@ -171,6 +171,16 @@ Proof.
+ destruct list_index; simpl. intuition easy. intuition.
Qed.
Lemma list_index_notin {A}`{EqbSpec A} (l : list A) x :
list_index x l = None <-> ~In x l.
Proof.
induction l as [|a l IH]; simpl.
- easy.
- case eqbspec.
+ intros <-. intuition discriminate.
+ destruct list_index; simpl. intuition easy. intuition.
Qed.
Lemma list_index_nth {A}`{EqbSpec A} (l : list A) n d :
NoDup l ->
n < List.length l ->
......
......@@ -8,6 +8,7 @@ Utils.v
Defs.v
Nam.v
Alpha.v
AlphaAlt.v
Mix.v
Proofs.v
Equiv.v
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment