reusing functions/defs for quotients

Stream: new members

[Logan Murphy]

Suppose I make a quotient type formulae based on some satisfaction relation

import data.set data.stream tactic
open set stream tactic

inductive base_formula (AP : Type)
| T : base_formula
| atom (a : AP) : base_formula
| conj (P Q : base_formula) : base_formula
| neg (P : base_formula) : base_formula

def inf_word (AP : Type)  : Type := stream (finset AP)

def sat  {AP : Type}
: inf_word AP → base_formula AP → Prop := sorry

def my_eqv_rel {AP : Type}  : base_formula AP → base_formula AP →  Prop := λ P Q,
{σ | sat σ P} = {σ | sat σ Q}

def base_formula_rel  (AP : Type) : setoid (base_formula AP) :=
 { r := my_eqv_rel,
  iseqv := sorry }

def formula (AP : Type) : Type := quotient (base_formula_rel AP)

I now want to prove some theorems about the satisfaction of formulae but I don't want to define a new satisfaction relation for formula, I want to use the same one I used to define the quotient type.

lemma new {AP : Type} (σ : inf_word AP) (Φ : formula AP) :
/- something to do with sat σ Φ --/ := sorry

Is this possible? Or is this misguided

[Logan Murphy]

I haven't been able to find a way to write a coercion from a quotient to its base type, does that exist?