Let x be given.
rewrite the current goal using
SNoL_0 (from left to right).
rewrite the current goal using
Repl_Empty (λw ⇒ w + x) (from left to right).
rewrite the current goal using
binunion_idl (from left to right).
Let u be given.
Let w be given.
We will
prove u ∈ SNoL x.
rewrite the current goal using H1 (from left to right).
rewrite the current goal using
IH w (SNoL_SNoS_ x w Hw) (from left to right).
We will
prove w ∈ SNoL x.
An exact proof term for the current goal is Hw.
Let u be given.
rewrite the current goal using
IH u (SNoL_SNoS_ x u Hu) (from right to left).
An
exact proof term for the current goal is
ReplI (SNoL x) (λw ⇒ 0 + w) u Hu.
rewrite the current goal using
SNoR_0 (from left to right).
rewrite the current goal using
Repl_Empty (λw ⇒ w + x) (from left to right).
rewrite the current goal using
binunion_idl (from left to right).
Let u be given.
Let w be given.
We will
prove u ∈ SNoR x.
rewrite the current goal using H1 (from left to right).
rewrite the current goal using
IH w (SNoR_SNoS_ x w Hw) (from left to right).
We will
prove w ∈ SNoR x.
An exact proof term for the current goal is Hw.
Let u be given.
rewrite the current goal using
IH u (SNoR_SNoS_ x u Hu) (from right to left).
An
exact proof term for the current goal is
ReplI (SNoR x) (λw ⇒ 0 + w) u Hu.
rewrite the current goal using L1 (from left to right).
rewrite the current goal using L2 (from left to right).
Use symmetry.
An
exact proof term for the current goal is
SNo_eta x Hx.
∎