proposition: Lemma start_pf j k ts1 ts2 (f2 : form j k ts2) : @raxiom j ts1 (untag f2) (subterm ts2 ts1) (equate f2).
proof: Proof. case: f2=>f2 [<- S A2] A1; rewrite (sc_interp S A1)=>V. case/(subterm_sound A2 (sc_wf S A1))=>xs. by case/domeqP; rewrite V=>/validL ->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options pred prelude) pcm(pcm unionmap natmap)