(15steps) PrintForm Definitions Lemmas mb automata 3 Sections GenAutomata Doc

At: rel subst2 tc


r:rel(), as:(LabelTerm) List, ds:Collection(dec()), da:Collection(SimpleType), de:sig(). tc(r;ds;da;de) (x:Label. (x rel_primed_vars(r)) (t:SimpleType. mk_dec(x, t) ds t term_types(ds;da;de;apply_alist(as;x;x)))) tc(rel_subst2(as;r);ds;da;de)

By: UnivCD

Generated subgoal:

11. r: rel()
2. as: (LabelTerm) List
3. ds: Collection(dec())
4. da: Collection(SimpleType)
5. de: sig()
6. tc(r;ds;da;de)
7. x:Label. (x rel_primed_vars(r)) (t:SimpleType. mk_dec(x, t) ds t term_types(ds;da;de;apply_alist(as;x;x)))
tc(rel_subst2(as;r);ds;da;de)


About:
productlistimpliesall

(15steps) PrintForm Definitions Lemmas mb automata 3 Sections GenAutomata Doc