Commit fe82f3a4 authored by Robbert Krebbers's avatar Robbert Krebbers

Simplify proof of fixpoint_unique.

parent 738d8bcc
Pipeline #2618 passed with stage
in 8 minutes and 55 seconds
......@@ -198,11 +198,9 @@ Section fixpoint.
Lemma fixpoint_unique (x : A) : x f x x fixpoint f.
Proof.
rewrite !equiv_dist=> Hx n.
rewrite fixpoint_eq /fixpoint_def (conv_compl n (fixpoint_chain f)) //=.
induction n as [|n IH]; simpl in *.
- rewrite Hx; eauto using contractive_0.
- rewrite Hx. apply (contractive_S _), IH.
rewrite !equiv_dist=> Hx n. induction n as [|n IH]; simpl in *.
- rewrite Hx fixpoint_unfold; eauto using contractive_0.
- rewrite Hx fixpoint_unfold. apply (contractive_S _), IH.
Qed.
Lemma fixpoint_ne (g : A A) `{!Contractive g} n :
......
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