val name_of_cipherSuite_of_name : (n: Parsers.CipherSuite.cipherSuite) -> Tot (squash (name_of_cipherSuite_of_name_post n))
val name_of_cipherSuite_of_name : (n: Parsers.CipherSuite.cipherSuite) -> Tot (squash (name_of_cipherSuite_of_name_post n))
let name_of_cipherSuite_of_name =
   _ by (
     let open FStar.Tactics in
     let n = intro () in
     destruct (binder_to_term n); 
     let _ = repeat (fun () -> iseq [fun () ->
       let breq = intro () in rewrite breq ; norm [delta; iota; zeta; primops]; trivial ()
     ])
     in
     let _ = intro () in
     let breq = intro () in
     rewrite breq;
     norm [delta; iota; zeta; primops];
     trivial ()
   )
module MiTLS.CipherSuite
open MiTLS
/
prims.fst.checked FStar.Tactics.Effect.fsti.checked FStar.Tactics.fst.checked FStar.Pervasives.fsti.checked
MiTLS.CipherSuite.fst
n: MiTLS.Parsers.CipherSuite.cipherSuite
  -> Prims.squash (MiTLS.CipherSuite.name_of_cipherSuite_of_name_post n)
MiTLS.Parsers.CipherSuite.cipherSuite FStar.UInt16.t Prims.b2t Prims.op_Negation MiTLS.Parsers.CipherSuite.known_cipherSuite_repr Prims.squash MiTLS.CipherSuite.name_of_cipherSuite_of_name_post
let name_of_cipherSuite_of_name =
  
FStar.Tactics.Effect.synth_by_tactic (fun _ ->
      (let open FStar.Tactics in
        let n = intro () in
        destruct (binder_to_term n);
        let _ =
          repeat (fun () ->
                iseq [
                    fun () ->
                      let breq = intro () in
                      rewrite breq;
                      norm [delta; iota; zeta; primops];
                      trivial ()
                  ])
        in
        let _ = intro () in
        let breq = intro () in
        rewrite breq;
        norm [delta; iota; zeta; primops];
        trivial ()))