Commit aff46e8d authored by Mário Pereira's avatar Mário Pereira
Browse files

Correct lemma permut_refl in theory seq.Permut

parent f16a2523
......@@ -369,6 +369,7 @@ theory Permut
(** {2 Lemmas about permut} *)
lemma permut_refl: forall s: seq 'a, l u: int.
0 <= l <= length s -> 0 <= u <= length s ->
permut s s l u
lemma permut_sym: forall s1 s2: seq 'a, l u: int.
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