| pc E1 E2 ⇒ (forget ? E1) · (forget ? E2)
| po E1 E2 ⇒ (forget ? E1) + (forget ? E2)
| pk E ⇒ (forget ? E)^* ].
-
+
+(* Already in the library
+notation "| term 19 C |" with precedence 70 for @{ 'card $C }.
+*)
interpretation "forget" 'card a = (forget ? a).
lemma erase_dot : ∀S.∀e1,e2:pitem S. |e1 · e2| = c ? (|e1|) (|e2|).
[/3/ | * * // #H1 #H2 @False_ind @(absurd …H1 H2)]
|>sem_pre_false normalize in ⊢ (??%?); #w % [ /3/ | * // ]
]
-qed.
\ No newline at end of file
+qed.