proposition: Lemma permut_tactic_trans : forall C l1 l2 l3, l3 = l2 -> C l1 l3 -> C l1 l2.
proof: Proof. Proof using. intros. subst~. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibRelation LibList LibInt LibNat LibOperation LibEpsilon LibSet LibMonoid)