trans tactic #
This implements the
trans tactic, which can apply transitivity theorems with an optional middle
tgt ← mkAppM' rel #[x, z] given
tgt = f z
tgt ← mkAppM' rel #[x, z] dropping more arguments if possible
trans applies to a goal whose target has the form
t ~ u where
~ is a transitive relation,
that is, a relation which has a transitivity lemma tagged with the attribute [trans].
trans sreplaces the goal with the two subgoals
t ~ sand
s ~ u.
sis omitted, then a metavariable is used instead.