Require Import Arith.

Set Implicit Arguments.

CoInductive cl : Set := Sk | K | app : cl -> cl -> cl .

Infix "$" := app (left associativity, at level 50).

Inductive rew : cl -> cl -> Set :=
 | k_rew : forall x y, rew (K $ x $ y) x
 | s_rew : forall x y z,
     rew (Sk $ x $ y $ z) ((x $ z) $ (y $ z))
 | trans : forall t tm t2,
     rew t tm -> rew tm t2 -> rew t t2
 | left : forall t t' r, rew t t' ->
     rew (t $ r) (t' $ r)
 | right : forall l t t', rew t t' ->
     rew (l $ t) (l $ t').

Definition I : cl := Sk $ K $ K.

Lemma iid : forall x, rew (I $ x) x.
Proof (fun x => trans (s_rew _ _ _) (k_rew _ _)).

Definition cl_open (c : cl) :=
  match c with
  | Sk => Sk
  | K => K
  | l $ r => l $ r
  end.

Lemma clo : forall c, c = cl_open c.
Proof (fun c =>
match c as c0 return c0 = cl_open c0 with
| Sk => eq_refl _
| K => eq_refl _
| l $ r => eq_refl _
end).

CoFixpoint SIw : cl := Sk $ I $ SIw.

Lemma SIw_unroll : SIw = Sk $ I $ SIw.
Proof (clo SIw).

Lemma siwfix : forall x, rew (SIw $ x) (x $ (SIw $ x)).
pattern SIw at 1.
rewrite SIw_unroll.
exact (fun x => trans
  (s_rew _ _ x)
  (left _ (iid x))).
Qed.