(* Below are a few, simple, semantic properties of items. In particular:
- not_epsilon_item : ∀S:DeqSet.∀i:pitem S. ¬ (\sem{i} ϵ).
- epsilon_pre : ∀S.∀e:pre S. (\sem{i} ϵ) ↔ (\snd e = true).
-- minus_eps_item: ∀S.∀i:pitem S. \sem{i} =1 \sem{i}-{[ ]}.
-- minus_eps_pre: ∀S.∀e:pre S. \sem{\fst e} =1 \sem{e}-{[ ]}.
+- minus_eps_item: ∀S.∀i:pitem S. \sem{i} ≐ \sem{i}-{[ ]}.
+- minus_eps_pre: ∀S.∀e:pre S. \sem{\fst e} ≐ \sem{e}-{[ ]}.
The first property is proved by a simple induction on $i$; the other
results are easy corollaries. We need an auxiliary lemma first. *)
#S * #i #b #btrue normalize in btrue; >btrue %2 //
qed.
-lemma minus_eps_item: ∀S.∀i:pitem S. \sem{i} ≐ \sem{i}-{[ ]}.
+lemma minus_eps_item: ∀S.∀i:pitem S. \sem{i} ≐ \sem{i}-{ϵ}.
#S #i #w %
[#H whd % // normalize @(not_to_not … (not_epsilon_lp …i)) //
|* //
]
qed.
-lemma minus_eps_pre: ∀S.∀e:pre S. \sem{fst ?? e} ≐ \sem{e}-{[ ]}.
+lemma minus_eps_pre: ∀S.∀e:pre S. \sem{fst ?? e} ≐ \sem{e}-{ϵ}.
#S * #i *
[>sem_pre_true normalize in ⊢ (??%?); #w %
[/3/ | * * // #H1 #H2 @False_ind @(absurd …H1 H2)]