Lemma proc_closed p : proc p → closed p.

Lemma proc_lambda p : proc p → lambda p.

Lemma equiv_trans_r (s t t' : term) : t == t' → s t == s t'.



Lemma database_dummy : I I I I I == I I I I I.